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₁[ Ordinal] means ( O1 c= $1 implies ConsecutiveDelta q,O1 c= ConsecutiveDelta q,$1 );
A1: S₁[ {} ] ;
A2: for O2 being Ordinal st S₁[O2] holds
S₁[ succ O2]

proof

let O2 be Ordinal; :: thesis: ( S₁[O2] implies S₁[ succ O2] )
assume A3: ( O1 c= O2 implies ConsecutiveDelta q,O1 c= ConsecutiveDelta q,O2 ) ; :: thesis: S₁[ succ O2]
assume A4: O1 c= succ O2 ; :: thesis: ConsecutiveDelta q,O1 c= ConsecutiveDelta q,(succ O2)

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

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

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

end;

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

then O1 c< succ O2 by A4, XBOOLE_0:def 8;
then A5: O1 in succ O2 by ORDINAL1:21;
ConsecutiveDelta q,(succ O2) = new_bi_fun (BiFun (ConsecutiveDelta q,O2),(ConsecutiveSet A,O2),L),(Quadr q,O2) by Th30
.= new_bi_fun (ConsecutiveDelta q,O2),(Quadr q,O2) by Def16 ;
then ConsecutiveDelta q,O2 c= ConsecutiveDelta q,(succ O2) by Th22;
hence ConsecutiveDelta q,O1 c= ConsecutiveDelta q,(succ O2) by A3, A5, ORDINAL1:34, XBOOLE_1:1; :: thesis: verum

end;

end;

end;

A6: for O2 being Ordinal st O2 <> {} & O2 is limit_ordinal & ( for O3 being Ordinal st O3 in O2 holds
S₁[O3] ) holds
S₁[O2]

proof

let O2 be Ordinal; :: thesis: ( O2 <> {} & O2 is limit_ordinal & ( for O3 being Ordinal st O3 in O2 holds
S₁[O3] ) implies S₁[O2] )
assume A7: ( O2 <> {} & O2 is limit_ordinal & ( for O3 being Ordinal st O3 in O2 & O1 c= O3 holds
ConsecutiveDelta q,O1 c= ConsecutiveDelta q,O3 ) ) ; :: thesis: S₁[O2]
assume A8: O1 c= O2 ; :: thesis: ConsecutiveDelta q,O1 c= ConsecutiveDelta q,O2
deffunc H₁( Ordinal) -> BiFunction of (ConsecutiveSet A,$1),L = ConsecutiveDelta q,$1;
consider L being T-Sequence such that
A9: ( dom L = O2 & ( for O3 being Ordinal st O3 in O2 holds
L . O3 = H₁(O3) ) ) from ORDINAL2:sch 2();
A10: ConsecutiveDelta q,O2 = union (rng L) by A7, A9, Th31;

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

suppose O1 = O2 ; :: thesis: ConsecutiveDelta q,O1 c= ConsecutiveDelta q,O2

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

end;

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

then A11: O1 c< O2 by A8, XBOOLE_0:def 8;
then A12: O1 in O2 by ORDINAL1:21;
A13: L . O1 = ConsecutiveDelta q,O1 by A9, A11, ORDINAL1:21;
L . O1 in rng L by A9, A12, FUNCT_1:def 5;
hence ConsecutiveDelta q,O1 c= ConsecutiveDelta q,O2 by A10, A13, ZFMISC_1:92; :: thesis: verum

end;

end;

end;

for O2 being Ordinal holds S₁[O2] from ORDINAL2:sch 1(A1, A2, A6);
hence ( O1 c= O2 implies ConsecutiveDelta q,O1 c= ConsecutiveDelta q,O2 ) ; :: thesis: verum