let X be set ; :: thesis: ( the_rank_of (Tarski-Class X) <> {} & the_rank_of (Tarski-Class X) is limit_ordinal )
A1: Tarski-Class X c= Rank (the_rank_of (Tarski-Class X)) by Def9;
thus the_rank_of (Tarski-Class X) <> {} :: thesis: the_rank_of (Tarski-Class X) is limit_ordinal
proof
assume the_rank_of (Tarski-Class X) = {} ; :: thesis: contradiction
then Tarski-Class X c= {} by Def9, Lm2;
hence contradiction ; :: thesis: verum
end;
assume not the_rank_of (Tarski-Class X) is limit_ordinal ; :: thesis: contradiction
then consider A being Ordinal such that
A2: the_rank_of (Tarski-Class X) = succ A by ORDINAL1:29;
consider Y being set such that
A3: Y in Tarski-Class X and
A4: the_rank_of Y = A by A2, Th72;
A5: bool Y in Tarski-Class X by A3, Th4;
A6: the_rank_of (bool Y) = succ A by A4, Th63;
bool Y c= Rank A by A1, A2, A5, Th32;
then succ A c= A by A6, Def9;
then A in A by ORDINAL1:21;
hence contradiction ; :: thesis: verum