הלמה של צורן הוא משפט שימושי העוסק בקבוצות סדורות חלקיות. המשפט שקול לאקסיומת הבחירה, במובן שניתן להוכיח אותו מאקסיומת הבחירה, ואם נקבל את המשפט כאקסיומה, נוכל להוכיח את אקסיומת הבחירה.
נניח בשלילה שלכל קיים כך ש. כלומר הקבוצה לא ריקה. מאקסיומת הבחירה קיימת פונקציה המתאימה לכל קבוצה כזו אחד מאיבריה. הרכבת הפונקציה על הפונקציה תתן פונקציה כך ש לכל .
תהי קבוצת כל השרשרות ב. מהנתון לכל , הקבוצה לא ריקה, לכן קיימת פונקציה המתאימה לכל קבוצה כזו אחד מאיבריה. הרכבת הפונקציה על הפונקציה תתן את הפונקציה עבורה לכל .
בהגדרתנו את הפונקציה על סודרים גבוליים, הנחנו כי היא שרשרת ולכן ניתן להפעיל עליה את הפונקציה . נראה זאת באמצעות שנוכיח כי הפונקציה היא שומרת סדר (כלומר ) עד (כלומר לכל מתקיים ), ולכן לכל מתקיים . נוכיח זאת באינדוקציה טרנספיניטית: עבור , הטענה מתקיימת באופן ריק. נניח נכונות עבור , ונוכיח עבור : אם , העניין ברור. לכן נניח כי . אם עוקב, אז . אם גבולי, אז גורר את , ומכיוון ש, ו חסם מלעיל של , נקבל . כעת נניח כי גבולי. אז , ומהנחת התכונה לכל , היא מתקיימת בפרט עבור , ולכן .
כשהוכחנו שהפונקציה מוגדרת, הוכחנו גם כי היא שומרת סדר, ובפרט חד-חד-ערכית (כי אם , אז או , ואז , או ש, ואז ). נגדיר על הקבוצה את הטענה . מאקסיומת ההחלפה נובע כי קיימת תמונת הטענה, אותה נסמן . קל לראות שלכל קיים סודר כך ש, ומכך ש חד חד ערכית נובע ש באופן יחיד. לכן הגדרת הטענה על הקבוצה תגרור, באמצעות אקסיומת ההחלפה, את קיום תמונת הטענה. כל סודר הוא בתמונת הטענה, כי מתקיים , לכן תמונת הטענה היא מחלקת כל הסודרים . מצד שני, מהפרדוקס של בורלי פורטי (טרם נכתב) נובע כי אינה קבוצה. סתירה.