 As for the AC, Gödel exhibits a definable well-ordering, that is, a formula of set theory which defines, in L, a well-ordering of all of L. The formula is tedious to write down but the idea is a simple one: A set x precedes a set y in the well-ordering if and only if either x occurs in the L-hierarchy on an earlier level Lα  than y, or else they occur on the same level but x is defined by a shorter formula than y, or else they are defined by the same formula but the parameters in the definition of x occur in L earlier than the parameters of y. This well-ordering of L shows that the AC holds in L.