for W being Universe
for a being Ordinal of W st a <> {} holds
Rank a is non empty Element of W by Th31, CLASSES1:36, ORDINAL3:8;