let A be non empty set ; :: thesis: for O, O1, O2 being Ordinal st O1 c= O2 holds
ConsecutiveSet2 (A,O1) c= ConsecutiveSet2 (A,O2)
let O, O1, 02 be Ordinal; :: thesis: ( O1 c= 02 implies ConsecutiveSet2 (A,O1) c= ConsecutiveSet2 (A,02) )
defpred S₁[ Ordinal] means ( O1 c= $1 implies ConsecutiveSet2 (A,O1) c= ConsecutiveSet2 (A,$1) );
A1: for O1 being Ordinal st S₁[O1] holds
S₁[ succ O1]

proof

let O2 be Ordinal; :: thesis: ( S₁[O2] implies S₁[ succ O2] )
assume A2: ( O1 c= O2 implies ConsecutiveSet2 (A,O1) c= ConsecutiveSet2 (A,O2) ) ; :: thesis: S₁[ succ O2]
assume A3: O1 c= succ O2 ; :: thesis: ConsecutiveSet2 (A,O1) c= ConsecutiveSet2 (A,(succ O2))

per cases ( O1 = succ O2 or O1 <> succ O2 ) ;

suppose O1 = succ O2 ; :: thesis: ConsecutiveSet2 (A,O1) c= ConsecutiveSet2 (A,(succ O2))

hence ConsecutiveSet2 (A,O1) c= ConsecutiveSet2 (A,(succ O2)) ; :: thesis: verum

end;

suppose O1 <> succ O2 ; :: thesis: ConsecutiveSet2 (A,O1) c= ConsecutiveSet2 (A,(succ O2))

then O1 c< succ O2 by A3, XBOOLE_0:def 8;
then A4: O1 in succ O2 by ORDINAL1:11;
ConsecutiveSet2 (A,O2) c= new_set2 (ConsecutiveSet2 (A,O2)) by XBOOLE_1:7;
then ConsecutiveSet2 (A,O1) c= new_set2 (ConsecutiveSet2 (A,O2)) by A2, A4, ORDINAL1:22, XBOOLE_1:1;
hence ConsecutiveSet2 (A,O1) c= ConsecutiveSet2 (A,(succ O2)) by Th16; :: thesis: verum

end;

end;

end;

A5: 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

deffunc H₁( Ordinal) -> set = ConsecutiveSet2 (A,$1);
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 that
A6: ( O2 <> {} & O2 is limit_ordinal ) and
for O3 being Ordinal st O3 in O2 & O1 c= O3 holds
ConsecutiveSet2 (A,O1) c= ConsecutiveSet2 (A,O3) ; :: thesis: S₁[O2]
consider L being T-Sequence such that
A7: ( dom L = O2 & ( for O3 being Ordinal st O3 in O2 holds
L . O3 = H₁(O3) ) ) from ORDINAL2:sch 2();
A8: ConsecutiveSet2 (A,O2) = union (rng L) by A6, A7, Th17;
assume A9: O1 c= O2 ; :: thesis: ConsecutiveSet2 (A,O1) c= ConsecutiveSet2 (A,O2)

per cases ( O1 = O2 or O1 <> O2 ) ;

suppose O1 = O2 ; :: thesis: ConsecutiveSet2 (A,O1) c= ConsecutiveSet2 (A,O2)

hence ConsecutiveSet2 (A,O1) c= ConsecutiveSet2 (A,O2) ; :: thesis: verum

end;

suppose O1 <> O2 ; :: thesis: ConsecutiveSet2 (A,O1) c= ConsecutiveSet2 (A,O2)

then A10: O1 c< O2 by A9, XBOOLE_0:def 8;
then O1 in O2 by ORDINAL1:11;
then A11: L . O1 in rng L by A7, FUNCT_1:def 3;
L . O1 = ConsecutiveSet2 (A,O1) by A7, A10, ORDINAL1:11;
hence ConsecutiveSet2 (A,O1) c= ConsecutiveSet2 (A,O2) by A8, A11, ZFMISC_1:74; :: thesis: verum

end;

end;

end;

A12: S₁[ {} ] ;
for O being Ordinal holds S₁[O] from ORDINAL2:sch 1(A12, A1, A5);
hence ( O1 c= 02 implies ConsecutiveSet2 (A,O1) c= ConsecutiveSet2 (A,02) ) ; :: thesis: verum