defpred S₁[ Ordinal] means not ConsecutiveSet2 A,A is empty;
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 not ConsecutiveSet2 A,O1 is empty ; :: thesis: S₁[ succ O1]
ConsecutiveSet2 A,(succ O1) = new_set2 (ConsecutiveSet2 A,O1) by Th16;
hence not ConsecutiveSet2 A,(succ O1) is empty ; :: thesis: verum

end;

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

end;

for O being Ordinal holds S₁[O] from ORDINAL2:sch 1(A1, A2, A3);
hence not ConsecutiveSet2 A,O is empty ; :: thesis: verum