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

end;

now

assume that
A5: A <> {} and
A6: for B being Ordinal holds A <> succ B ; :: thesis: union X in Rank A
A7: A is limit_ordinal by A6, ORDINAL1:29;
then consider B being Ordinal such that
A8: B in A and
A9: X in Rank B by A1, A5, Th35;
X c= Rank B by A9, ORDINAL1:def 2;
then A10: union X c= union (Rank B) by ZFMISC_1:77;
union (Rank B) c= Rank B by Th40;
then A11: union X c= Rank B by A10, XBOOLE_1:1;
A12: succ B c= A by A8, ORDINAL1:21;
succ B <> A by A6;
then A13: succ B c< A by A12, XBOOLE_0:def 8;
A14: union X in Rank (succ B) by A11, Th36;
succ B in A by A13, ORDINAL1:11;
hence union X in Rank A by A7, A14, Th35; :: thesis: verum

end;

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