let X be set ; :: thesis: for A being Ordinal st X in Rank A holds
union X in Rank A
let A be Ordinal; :: thesis: ( X in Rank A implies union X in Rank A )
assume A1: X in Rank A ; :: thesis: union X in Rank A

A2: now

given B being Ordinal such that A3: A = succ B ; :: thesis: union X in Rank A
X c= Rank B by A1, A3, Th36;
then ( union X c= union (Rank B) & union (Rank B) c= Rank B ) by Th40, ZFMISC_1:95;
then union X c= Rank B by XBOOLE_1:1;
hence union X in Rank A by A3, Th36; :: thesis: verum

end;

now

assume A4: ( A <> {} & ( for B being Ordinal holds A <> succ B ) ) ; :: thesis: union X in Rank A
then A5: A is limit_ordinal by ORDINAL1:42;
then consider B being Ordinal such that
A6: ( B in A & X in Rank B ) by A1, A4, Th35;
X c= Rank B by A6, ORDINAL1:def 2;
then ( union X c= union (Rank B) & union (Rank B) c= Rank B ) by Th40, ZFMISC_1:95;
then A7: ( union X c= Rank B & succ B c= A & succ B <> A ) by A4, A6, ORDINAL1:33, XBOOLE_1:1;
then succ B c< A by XBOOLE_0:def 8;
then ( union X in Rank (succ B) & succ B in A ) by A7, Th36, ORDINAL1:21;
hence union X in Rank A by A5, Th35; :: thesis: verum

end;

hence union X in Rank A by A1, A2, Lm2; :: thesis: verum