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 S1[ 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
S1[O3] ) holds
S1[O2]
proof
deffunc H1( 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
S1[O3] ) implies S1[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: S1[O2]
consider L being Sequence such that
A3: ( dom L = O2 & ( for O3 being Ordinal st O3 in O2 holds
L . O3 = H1(O3) ) ) from 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;
end;
A8: for O2 being Ordinal st S1[O2] holds
S1[ succ O2]
proof end;
A12: S1[ 0 ] ;
for O2 being Ordinal holds S1[O2] from hence ( O1 c= O2 implies ConsecutiveDelta (q,O1) c= ConsecutiveDelta (q,O2) ) ; :: thesis: verum