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 :: thesis: ( ex B being Ordinal st A = succ B implies X in Rank A )
given B being Ordinal such that A4: A = succ B ; :: thesis: X in Rank A
A5: Rank (succ B) = bool (Rank B) by Lm2;
then X c= Rank B by A1, A2, A4, XBOOLE_1:1;
hence X in Rank A by A4, A5; :: thesis: verum
end;
now :: thesis: ( ( for B being Ordinal holds A <> succ B ) implies X in Rank A )
assume A6: for B being Ordinal holds A <> succ B ; :: thesis: X in Rank A
then A7: A is limit_ordinal by ORDINAL1:29;
then consider B being Ordinal such that
A8: B in A and
A9: Y in Rank B by A2, Lm2, Th31;
Y c= Rank B by A9, ORDINAL1:def 2;
then A10: X c= Rank B by A1;
A11: bool (Rank B) = Rank (succ B) by Lm2;
succ B in A by A6, A8, ORDINAL1:28, ORDINAL1:29;
hence X in Rank A by A7, A10, A11, Th31; :: thesis: verum
end;
hence X in Rank A by A3; :: thesis: verum