let A be non empty set ; :: thesis: for O1, O2 being Ordinal st O1 c= O2 holds

ConsecutiveSet (A,O1) c= ConsecutiveSet (A,O2)

let O1, O2 be Ordinal; :: thesis: ( O1 c= O2 implies ConsecutiveSet (A,O1) c= ConsecutiveSet (A,O2) )

defpred S_{1}[ Ordinal] means ( O1 c= $1 implies ConsecutiveSet (A,O1) c= ConsecutiveSet (A,$1) );

A1: for O2 being Ordinal st S_{1}[O2] holds

S_{1}[ succ O2]

S_{1}[O3] ) holds

S_{1}[O2]
_{1}[ 0 ]
;

for O2 being Ordinal holds S_{1}[O2]
from ORDINAL2:sch 1(A12, A1, A5);

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

ConsecutiveSet (A,O1) c= ConsecutiveSet (A,O2)

let O1, O2 be Ordinal; :: thesis: ( O1 c= O2 implies ConsecutiveSet (A,O1) c= ConsecutiveSet (A,O2) )

defpred S

A1: for O2 being Ordinal st S

S

proof

A5:
for O2 being Ordinal st O2 <> 0 & O2 is limit_ordinal & ( for O3 being Ordinal st O3 in O2 holds
let O2 be Ordinal; :: thesis: ( S_{1}[O2] implies S_{1}[ succ O2] )

assume A2: ( O1 c= O2 implies ConsecutiveSet (A,O1) c= ConsecutiveSet (A,O2) ) ; :: thesis: S_{1}[ succ O2]

assume A3: O1 c= succ O2 ; :: thesis: ConsecutiveSet (A,O1) c= ConsecutiveSet (A,(succ O2))

end;assume A2: ( O1 c= O2 implies ConsecutiveSet (A,O1) c= ConsecutiveSet (A,O2) ) ; :: thesis: S

assume A3: O1 c= succ O2 ; :: thesis: ConsecutiveSet (A,O1) c= ConsecutiveSet (A,(succ O2))

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

end;

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

then
O1 c< succ O2
by A3;

then A4: O1 in succ O2 by ORDINAL1:11;

ConsecutiveSet (A,O2) c= new_set (ConsecutiveSet (A,O2)) by XBOOLE_1:7;

then ConsecutiveSet (A,O1) c= new_set (ConsecutiveSet (A,O2)) by A2, A4, ORDINAL1:22;

hence ConsecutiveSet (A,O1) c= ConsecutiveSet (A,(succ O2)) by Th22; :: thesis: verum

end;then A4: O1 in succ O2 by ORDINAL1:11;

ConsecutiveSet (A,O2) c= new_set (ConsecutiveSet (A,O2)) by XBOOLE_1:7;

then ConsecutiveSet (A,O1) c= new_set (ConsecutiveSet (A,O2)) by A2, A4, ORDINAL1:22;

hence ConsecutiveSet (A,O1) c= ConsecutiveSet (A,(succ O2)) by Th22; :: thesis: verum

S

S

proof

A12:
S
deffunc H_{1}( Ordinal) -> set = ConsecutiveSet (A,$1);

let O2 be Ordinal; :: thesis: ( O2 <> 0 & O2 is limit_ordinal & ( for O3 being Ordinal st O3 in O2 holds

S_{1}[O3] ) implies S_{1}[O2] )

assume that

A6: ( O2 <> 0 & O2 is limit_ordinal ) and

for O3 being Ordinal st O3 in O2 & O1 c= O3 holds

ConsecutiveSet (A,O1) c= ConsecutiveSet (A,O3) ; :: thesis: S_{1}[O2]

consider L being Sequence such that

A7: ( dom L = O2 & ( for O3 being Ordinal st O3 in O2 holds

L . O3 = H_{1}(O3) ) )
from ORDINAL2:sch 2();

A8: ConsecutiveSet (A,O2) = union (rng L) by A6, A7, Th23;

assume A9: O1 c= O2 ; :: thesis: ConsecutiveSet (A,O1) c= ConsecutiveSet (A,O2)

end;let O2 be Ordinal; :: thesis: ( O2 <> 0 & O2 is limit_ordinal & ( for O3 being Ordinal st O3 in O2 holds

S

assume that

A6: ( O2 <> 0 & O2 is limit_ordinal ) and

for O3 being Ordinal st O3 in O2 & O1 c= O3 holds

ConsecutiveSet (A,O1) c= ConsecutiveSet (A,O3) ; :: thesis: S

consider L being Sequence such that

A7: ( dom L = O2 & ( for O3 being Ordinal st O3 in O2 holds

L . O3 = H

A8: ConsecutiveSet (A,O2) = union (rng L) by A6, A7, Th23;

assume A9: O1 c= O2 ; :: thesis: ConsecutiveSet (A,O1) c= ConsecutiveSet (A,O2)

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

end;

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

then A10:
O1 c< O2
by A9;

then O1 in O2 by ORDINAL1:11;

then A11: L . O1 in rng L by A7, FUNCT_1:def 3;

L . O1 = ConsecutiveSet (A,O1) by A7, A10, ORDINAL1:11;

hence ConsecutiveSet (A,O1) c= ConsecutiveSet (A,O2) by A8, A11, ZFMISC_1:74; :: thesis: verum

end;then O1 in O2 by ORDINAL1:11;

then A11: L . O1 in rng L by A7, FUNCT_1:def 3;

L . O1 = ConsecutiveSet (A,O1) by A7, A10, ORDINAL1:11;

hence ConsecutiveSet (A,O1) c= ConsecutiveSet (A,O2) by A8, A11, ZFMISC_1:74; :: thesis: verum

for O2 being Ordinal holds S

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