let A be non empty set ; :: thesis: for L being lower-bounded LATTICE
for d being BiFunction of A,L
for O1, O2 being Ordinal
for q being QuadrSeq of d st O1 c= O2 holds
ConsecutiveDelta2 (q,O1) c= ConsecutiveDelta2 (q,O2)
let L be lower-bounded LATTICE; :: thesis: for d being BiFunction of A,L
for O1, O2 being Ordinal
for q being QuadrSeq of d st O1 c= O2 holds
ConsecutiveDelta2 (q,O1) c= ConsecutiveDelta2 (q,O2)
let d be BiFunction of A,L; :: thesis: for O1, O2 being Ordinal
for q being QuadrSeq of d st O1 c= O2 holds
ConsecutiveDelta2 (q,O1) c= ConsecutiveDelta2 (q,O2)
let O1, O2 be Ordinal; :: thesis: for q being QuadrSeq of d st O1 c= O2 holds
ConsecutiveDelta2 (q,O1) c= ConsecutiveDelta2 (q,O2)
let q be QuadrSeq of d; :: thesis: ( O1 c= O2 implies ConsecutiveDelta2 (q,O1) c= ConsecutiveDelta2 (q,O2) )
defpred S₁[ Ordinal] means ( O1 c= $1 implies ConsecutiveDelta2 (q,O1) c= ConsecutiveDelta2 (q,$1) );
A1: for O1 being Ordinal st O1 <> 0 & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds
S₁[O2] ) holds
S₁[O1]

proof

deffunc H₁( Ordinal) -> BiFunction of (ConsecutiveSet2 (A,$1)),L = ConsecutiveDelta2 (q,$1);
let O2 be Ordinal; :: thesis: ( O2 <> 0 & O2 is limit_ordinal & ( for O2 being Ordinal st O2 in O2 holds
S₁[O2] ) implies S₁[O2] )
assume that
A2: ( O2 <> 0 & O2 is limit_ordinal ) and
for O3 being Ordinal st O3 in O2 & O1 c= O3 holds
ConsecutiveDelta2 (q,O1) c= ConsecutiveDelta2 (q,O3) ; :: thesis: S₁[O2]
consider L being Sequence such that
A3: ( dom L = O2 & ( for O3 being Ordinal st O3 in O2 holds
L . O3 = H₁(O3) ) ) from ORDINAL2:sch 2();
A4: ConsecutiveDelta2 (q,O2) = union (rng L) by A2, A3, Th20;
assume A5: O1 c= O2 ; :: thesis: ConsecutiveDelta2 (q,O1) c= ConsecutiveDelta2 (q,O2)

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

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

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

end;

suppose O1 <> O2 ; :: thesis: ConsecutiveDelta2 (q,O1) c= ConsecutiveDelta2 (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 = ConsecutiveDelta2 (q,O1) by A3, A6, ORDINAL1:11;
hence ConsecutiveDelta2 (q,O1) c= ConsecutiveDelta2 (q,O2) by A4, A7, ZFMISC_1:74; :: thesis: verum

end;

end;

end;

A8: for O1 being Ordinal st S₁[O1] holds
S₁[ succ O1]

proof

let O2 be Ordinal; :: thesis: ( S₁[O2] implies S₁[ succ O2] )
assume A9: ( O1 c= O2 implies ConsecutiveDelta2 (q,O1) c= ConsecutiveDelta2 (q,O2) ) ; :: thesis: S₁[ succ O2]
assume A10: O1 c= succ O2 ; :: thesis: ConsecutiveDelta2 (q,O1) c= ConsecutiveDelta2 (q,(succ O2))

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

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

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

end;

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

ConsecutiveDelta2 (q,(succ O2)) = new_bi_fun2 ((BiFun ((ConsecutiveDelta2 (q,O2)),(ConsecutiveSet2 (A,O2)),L)),(Quadr2 (q,O2))) by Th19
.= new_bi_fun2 ((ConsecutiveDelta2 (q,O2)),(Quadr2 (q,O2))) by LATTICE5:def 15 ;
then A12: ConsecutiveDelta2 (q,O2) c= ConsecutiveDelta2 (q,(succ O2)) by Th13;
O1 c< succ O2 by A10, A11;
then O1 in succ O2 by ORDINAL1:11;
hence ConsecutiveDelta2 (q,O1) c= ConsecutiveDelta2 (q,(succ O2)) by A9, A12, ORDINAL1:22; :: thesis: verum

end;

end;

end;

A13: S₁[ 0 ] ;
for O being Ordinal holds S₁[O] from ORDINAL2:sch 1(A13, A8, A1);
hence ( O1 c= O2 implies ConsecutiveDelta2 (q,O1) c= ConsecutiveDelta2 (q,O2) ) ; :: thesis: verum