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

end;

A8: 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;
consider B being Ordinal such that
A12: B in A and
A13: X in Rank B by A1, A9, A11, Th35;
A14: X c= Rank B by A13, ORDINAL1:def 2;
A15: union X c= union (Rank B) by A14, ZFMISC_1:95;
A16: union (Rank B) c= Rank B by Th40;
A17: union X c= Rank B by A15, A16, XBOOLE_1:1;
A18: succ B c= A by A12, ORDINAL1:33;
A19: succ B <> A by A10;
A20: succ B c< A by A18, A19, XBOOLE_0:def 8;
A21: union X in Rank (succ B) by A17, Th36;
A22: succ B in A by A20, ORDINAL1:21;
thus union X in Rank A by A11, A21, A22, Th35; :: thesis: verum

end;

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