let W be Universe; :: thesis: for a being Ordinal of W st a <> {} holds
Rank a is non empty Element of W
let a be Ordinal of W; :: thesis: ( a <> {} implies Rank a is non empty Element of W )
assume a <> {} ; :: thesis: Rank a is non empty Element of W
then {} in a by ORDINAL3:10;
then reconsider D = Rank a as non empty set by CLASSES1:42;
D in W by Th33;
hence Rank a is non empty Element of W ; :: thesis: verum