 Not only ZF but also Kelley-Morse class theory can be interpreted; any definable class of well-founded sets has a closure whose well-founded members will be exactly the desired members (it will as a rule have other, non-well-founded members). Quantification over these “classes” defines sets just as easily as quantification over mere sets in this context; so we get an impredicative class theory. Further, one can prove internally to this theory that the “proper class ordinal” in the interpreted \(KM\) has the tree property, and so is in effect a weakly compact cardinal; this shows that this theory has considerable consistency strength (for example, its version of ZF proves that there is a proper class of inaccessible cardinals, a proper class of \(n\)-Mahlos for each \(n\), and so forth): the use of large cardinals in the outlined model construction above was essential.