let A be non empty Ordinal; :: thesis: not Rank A is empty
( A <> {} & {} c= A ) by XBOOLE_1:2;
then {} c< A by XBOOLE_0:def 8;
then {} in A by ORDINAL1:21;
hence not Rank A is empty by CLASSES1:42; :: thesis: verum