defpred S1[ Ordinal] means not ConsecutiveSet (A,A) is empty ;
A1: for O being Ordinal st S1[O] holds
S1[ succ O]
proof
let O1 be Ordinal; :: thesis: ( S1[O1] implies S1[ succ O1] )
assume not ConsecutiveSet (A,O1) is empty ; :: thesis: S1[ succ O1]
ConsecutiveSet (A,(succ O1)) = new_set (ConsecutiveSet (A,O1)) by Th22;
hence S1[ succ O1] ; :: thesis: verum
end;
A2: for O being Ordinal st O <> 0 & O is limit_ordinal & ( for B being Ordinal st B in O holds
S1[B] ) holds
S1[O]
proof
deffunc H1( Ordinal) -> set = ConsecutiveSet (A,A);
let O1 be Ordinal; :: thesis: ( O1 <> 0 & O1 is limit_ordinal & ( for B being Ordinal st B in O1 holds
S1[B] ) implies S1[O1] )
assume that
A3: O1 <> 0 and
A4: O1 is limit_ordinal and
for O2 being Ordinal st O2 in O1 holds
not ConsecutiveSet (A,O2) is empty ; :: thesis: S1[O1]
A5: {} in O1 by A3, ORDINAL3:8;
consider Ls being Sequence such that
A6: ( dom Ls = O1 & ( for O2 being Ordinal st O2 in O1 holds
Ls . O2 = H1(O2) ) ) from ORDINAL2:sch 2();
 Ls . {} = ConsecutiveSet (A,{}) by A3, A6, ORDINAL3:8
.= A by Th21 ;
then A7: A in rng Ls by A6, A5, FUNCT_1:def 3;
ConsecutiveSet (A,O1) = union (rng Ls) by A3, A4, A6, Th23;
then A c= ConsecutiveSet (A,O1) by A7, ZFMISC_1:74;
hence S1[O1] ; :: thesis: verum
end;
A8: S1[ 0 ] by Th21;
for O being Ordinal holds S1[O] from ORDINAL2:sch 1(A8, A1, A2);
 hence not ConsecutiveSet (A,O) is empty ; :: thesis: verum