let A be non empty Ordinal; :: thesis: not Rank A is empty

{} c= A ;

then {} c< A by XBOOLE_0:def 8;

then {} in A by ORDINAL1:11;

hence not Rank A is empty by CLASSES1:36; :: thesis: verum

{} c= A ;

then {} c< A by XBOOLE_0:def 8;

then {} in A by ORDINAL1:11;

hence not Rank A is empty by CLASSES1:36; :: thesis: verum