defpred S₁[ Ordinal] means not ConsecutiveSet A,A is empty ;
A1: for O being Ordinal st S₁[O] holds
S₁[ succ O]

proof

let O1 be Ordinal; :: thesis: ( S₁[O1] implies S₁[ succ O1] )
assume not ConsecutiveSet A,O1 is empty ; :: thesis: S₁[ succ O1]
ConsecutiveSet A,(succ O1) = new_set (ConsecutiveSet A,O1) by Th25;
hence S₁[ succ O1] ; :: thesis: verum

end;

A2: for O being Ordinal st O <> {} & O is limit_ordinal & ( for B being Ordinal st B in O holds
S₁[B] ) holds
S₁[O]

proof

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

end;

A8: S₁[ {} ] by Th24;
for O being Ordinal holds S₁[O] from ORDINAL2:sch 1(A8, A1, A2);
hence not ConsecutiveSet A,O is empty ; :: thesis: verum