let A be non empty set ; :: thesis: for O being Ordinal holds A c= ConsecutiveSet2 A,O
let O be Ordinal; :: thesis: A c= ConsecutiveSet2 A,O
defpred S₁[ Ordinal] means A c= ConsecutiveSet2 A,$1;
A1: S₁[ {} ] by Th15;
A2: for O1 being Ordinal st S₁[O1] holds
S₁[ succ O1]

proof

let O1 be Ordinal; :: thesis: ( S₁[O1] implies S₁[ succ O1] )
assume A3: A c= ConsecutiveSet2 A,O1 ; :: thesis: S₁[ succ O1]
ConsecutiveSet2 A,(succ O1) = new_set2 (ConsecutiveSet2 A,O1) by Th16;
then ConsecutiveSet2 A,O1 c= ConsecutiveSet2 A,(succ O1) by XBOOLE_1:7;
hence S₁[ succ O1] by A3, XBOOLE_1:1; :: thesis: verum

end;

A4: for O1 being Ordinal st O1 <> {} & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds
S₁[O2] ) holds
S₁[O1]

proof

let O2 be Ordinal; :: thesis: ( O2 <> {} & O2 is limit_ordinal & ( for O2 being Ordinal st O2 in O2 holds
S₁[O2] ) implies S₁[O2] )
assume A5: ( O2 <> {} & O2 is limit_ordinal & ( for O1 being Ordinal st O1 in O2 holds
A c= ConsecutiveSet2 A,O1 ) ) ; :: thesis: S₁[O2]
deffunc H₁( Ordinal) -> set = ConsecutiveSet2 A,$1;
consider Ls being T-Sequence such that
A6: ( dom Ls = O2 & ( for O1 being Ordinal st O1 in O2 holds
Ls . O1 = H₁(O1) ) ) from ORDINAL2:sch 2();
A7: ConsecutiveSet2 A,O2 = union (rng Ls) by A5, A6, Th17;
A8: {} in O2 by A5, ORDINAL3:10;
then Ls . {} = ConsecutiveSet2 A,{} by A6
.= A by Th15 ;
then A in rng Ls by A6, A8, FUNCT_1:def 5;
hence S₁[O2] by A7, ZFMISC_1:92; :: thesis: verum

end;

for O being Ordinal holds S₁[O] from ORDINAL2:sch 1(A1, A2, A4);
hence A c= ConsecutiveSet2 A,O ; :: thesis: verum