let X, Y be set ; :: thesis: for A being Ordinal st X c= Y & Y in Rank A holds
X in Rank A
let A be Ordinal; :: thesis: ( X c= Y & Y in Rank A implies X in Rank A )
assume A1: ( X c= Y & Y in Rank A ) ; :: thesis: X in Rank A

A2: now

given B being Ordinal such that A3: A = succ B ; :: thesis: X in Rank A
A4: Rank (succ B) = bool (Rank B) by Lm2;
then X c= Rank B by A1, A3, XBOOLE_1:1;
hence X in Rank A by A3, A4; :: thesis: verum

end;

now

assume for B being Ordinal holds A <> succ B ; :: thesis: X in Rank A
then A5: A is limit_ordinal by ORDINAL1:42;
then consider B being Ordinal such that
A6: ( B in A & Y in Rank B ) by A1, Lm2, Th35;
Y c= Rank B by A6, ORDINAL1:def 2;
then X c= Rank B by A1, XBOOLE_1:1;
then ( X in bool (Rank B) & bool (Rank B) = Rank (succ B) & succ B in A ) by A5, A6, Lm2, ORDINAL1:41;
hence X in Rank A by A5, Th35; :: thesis: verum

end;

hence X in Rank A by A2; :: thesis: verum