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 A5: union X c= union (Rank B) by ZFMISC_1:95;
union (Rank B) c= Rank B by Th40;
then union X c= Rank B by A5, XBOOLE_1:1;
hence union X in Rank A by A3, Th36; :: thesis: verum

end;

now

assume that
A9: A <> {} and
A10: for B being Ordinal holds A <> succ B ; :: thesis: union X in Rank A
A11: A is limit_ordinal by A10, ORDINAL1:42;
then consider B being Ordinal such that
A12: B in A and
A13: X in Rank B by A1, A9, Th35;
X c= Rank B by A13, ORDINAL1:def 2;
then A15: union X c= union (Rank B) by ZFMISC_1:95;
union (Rank B) c= Rank B by Th40;
then A17: union X c= Rank B by A15, XBOOLE_1:1;
A18: succ B c= A by A12, ORDINAL1:33;
succ B <> A by A10;
then A20: succ B c< A by A18, XBOOLE_0:def 8;
A21: union X in Rank (succ B) by A17, Th36;
succ B in A by A20, ORDINAL1:21;
hence union X in Rank A by A11, A21, Th35; :: thesis: verum

end;

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