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