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 that
A1: X c= Y and
A2: Y in Rank A ; :: thesis: X in Rank A

A3: now

given B being Ordinal such that A4: A = succ B ; :: thesis: X in Rank A
A5: Rank (succ B) = bool (Rank B) by Lm2;
A6: X c= Rank B by A1, A2, A4, A5, XBOOLE_1:1;
thus X in Rank A by A4, A5, A6; :: thesis: verum

end;

A7: now

assume A8: for B being Ordinal holds A <> succ B ; :: thesis: X in Rank A
A9: A is limit_ordinal by A8, ORDINAL1:42;
consider B being Ordinal such that
A10: B in A and
A11: Y in Rank B by A2, A9, Lm2, Th35;
A12: Y c= Rank B by A11, ORDINAL1:def 2;
A13: X c= Rank B by A1, A12, XBOOLE_1:1;
A14: bool (Rank B) = Rank (succ B) by Lm2;
A15: succ B in A by A9, A10, ORDINAL1:41;
thus X in Rank A by A9, A13, A14, A15, Th35; :: thesis: verum

end;

thus X in Rank A by A3, A7; :: thesis: verum