let A be non empty set ; :: thesis: for L being lower-bounded LATTICE

for O1, O2 being Ordinal

for d being BiFunction of A,L

for q being QuadrSeq of d st O1 c= O2 holds

ConsecutiveDelta (q,O1) c= ConsecutiveDelta (q,O2)

let L be lower-bounded LATTICE; :: thesis: for O1, O2 being Ordinal

for d being BiFunction of A,L

for q being QuadrSeq of d st O1 c= O2 holds

ConsecutiveDelta (q,O1) c= ConsecutiveDelta (q,O2)

let O1, O2 be Ordinal; :: thesis: for d being BiFunction of A,L

for q being QuadrSeq of d st O1 c= O2 holds

ConsecutiveDelta (q,O1) c= ConsecutiveDelta (q,O2)

let d be BiFunction of A,L; :: thesis: for q being QuadrSeq of d st O1 c= O2 holds

ConsecutiveDelta (q,O1) c= ConsecutiveDelta (q,O2)

let q be QuadrSeq of d; :: thesis: ( O1 c= O2 implies ConsecutiveDelta (q,O1) c= ConsecutiveDelta (q,O2) )

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

A1: for O2 being Ordinal st O2 <> 0 & O2 is limit_ordinal & ( for O3 being Ordinal st O3 in O2 holds

S_{1}[O3] ) holds

S_{1}[O2]
_{1}[O2] holds

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

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

hence ( O1 c= O2 implies ConsecutiveDelta (q,O1) c= ConsecutiveDelta (q,O2) ) ; :: thesis: verum

for O1, O2 being Ordinal

for d being BiFunction of A,L

for q being QuadrSeq of d st O1 c= O2 holds

ConsecutiveDelta (q,O1) c= ConsecutiveDelta (q,O2)

let L be lower-bounded LATTICE; :: thesis: for O1, O2 being Ordinal

for d being BiFunction of A,L

for q being QuadrSeq of d st O1 c= O2 holds

ConsecutiveDelta (q,O1) c= ConsecutiveDelta (q,O2)

let O1, O2 be Ordinal; :: thesis: for d being BiFunction of A,L

for q being QuadrSeq of d st O1 c= O2 holds

ConsecutiveDelta (q,O1) c= ConsecutiveDelta (q,O2)

let d be BiFunction of A,L; :: thesis: for q being QuadrSeq of d st O1 c= O2 holds

ConsecutiveDelta (q,O1) c= ConsecutiveDelta (q,O2)

let q be QuadrSeq of d; :: thesis: ( O1 c= O2 implies ConsecutiveDelta (q,O1) c= ConsecutiveDelta (q,O2) )

defpred S

A1: for O2 being Ordinal st O2 <> 0 & O2 is limit_ordinal & ( for O3 being Ordinal st O3 in O2 holds

S

S

proof

A8:
for O2 being Ordinal st S
deffunc H_{1}( Ordinal) -> BiFunction of (ConsecutiveSet (A,$1)),L = ConsecutiveDelta (q,$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

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

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

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

consider L being Sequence such that

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

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

A4: ConsecutiveDelta (q,O2) = union (rng L) by A2, A3, Th28;

assume A5: O1 c= O2 ; :: thesis: ConsecutiveDelta (q,O1) c= ConsecutiveDelta (q,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

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

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

ConsecutiveDelta (q,O1) c= ConsecutiveDelta (q,O3) ; :: thesis: S

consider L being Sequence such that

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

L . O3 = H

A4: ConsecutiveDelta (q,O2) = union (rng L) by A2, A3, Th28;

assume A5: O1 c= O2 ; :: thesis: ConsecutiveDelta (q,O1) c= ConsecutiveDelta (q,O2)

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

end;

suppose
O1 <> O2
; :: thesis: ConsecutiveDelta (q,O1) c= ConsecutiveDelta (q,O2)

then A6:
O1 c< O2
by A5;

then O1 in O2 by ORDINAL1:11;

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

L . O1 = ConsecutiveDelta (q,O1) by A3, A6, ORDINAL1:11;

hence ConsecutiveDelta (q,O1) c= ConsecutiveDelta (q,O2) by A4, A7, ZFMISC_1:74; :: thesis: verum

end;then O1 in O2 by ORDINAL1:11;

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

L . O1 = ConsecutiveDelta (q,O1) by A3, A6, ORDINAL1:11;

hence ConsecutiveDelta (q,O1) c= ConsecutiveDelta (q,O2) by A4, A7, ZFMISC_1:74; :: thesis: verum

S

proof

A12:
S
let O2 be Ordinal; :: thesis: ( S_{1}[O2] implies S_{1}[ succ O2] )

assume A9: ( O1 c= O2 implies ConsecutiveDelta (q,O1) c= ConsecutiveDelta (q,O2) ) ; :: thesis: S_{1}[ succ O2]

assume A10: O1 c= succ O2 ; :: thesis: ConsecutiveDelta (q,O1) c= ConsecutiveDelta (q,(succ O2))

end;assume A9: ( O1 c= O2 implies ConsecutiveDelta (q,O1) c= ConsecutiveDelta (q,O2) ) ; :: thesis: S

assume A10: O1 c= succ O2 ; :: thesis: ConsecutiveDelta (q,O1) c= ConsecutiveDelta (q,(succ O2))

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

end;

suppose
O1 <> succ O2
; :: thesis: ConsecutiveDelta (q,O1) c= ConsecutiveDelta (q,(succ O2))

then
O1 c< succ O2
by A10;

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

ConsecutiveDelta (q,(succ O2)) = new_bi_fun ((BiFun ((ConsecutiveDelta (q,O2)),(ConsecutiveSet (A,O2)),L)),(Quadr (q,O2))) by Th27

.= new_bi_fun ((ConsecutiveDelta (q,O2)),(Quadr (q,O2))) by Def15 ;

then ConsecutiveDelta (q,O2) c= ConsecutiveDelta (q,(succ O2)) by Th19;

hence ConsecutiveDelta (q,O1) c= ConsecutiveDelta (q,(succ O2)) by A9, A11, ORDINAL1:22; :: thesis: verum

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

ConsecutiveDelta (q,(succ O2)) = new_bi_fun ((BiFun ((ConsecutiveDelta (q,O2)),(ConsecutiveSet (A,O2)),L)),(Quadr (q,O2))) by Th27

.= new_bi_fun ((ConsecutiveDelta (q,O2)),(Quadr (q,O2))) by Def15 ;

then ConsecutiveDelta (q,O2) c= ConsecutiveDelta (q,(succ O2)) by Th19;

hence ConsecutiveDelta (q,O1) c= ConsecutiveDelta (q,(succ O2)) by A9, A11, ORDINAL1:22; :: thesis: verum

for O2 being Ordinal holds S

hence ( O1 c= O2 implies ConsecutiveDelta (q,O1) c= ConsecutiveDelta (q,O2) ) ; :: thesis: verum