let A be non empty set ; 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; 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; 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; for q being QuadrSeq of d st O1 c= O2 holds
ConsecutiveDelta2 (q,O1) c= ConsecutiveDelta2 (q,O2)
let q be QuadrSeq of d; ( O1 c= O2 implies ConsecutiveDelta2 (q,O1) c= ConsecutiveDelta2 (q,O2) )
defpred S1[ 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
S1[O2] ) holds
S1[O1]
proof
deffunc H1(
Ordinal)
-> BiFunction of
(ConsecutiveSet2 (A,$1)),
L =
ConsecutiveDelta2 (
q,$1);
let O2 be
Ordinal;
( O2 <> 0 & O2 is limit_ordinal & ( for O2 being Ordinal st O2 in O2 holds
S1[O2] ) 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
ConsecutiveDelta2 (
q,
O1)
c= ConsecutiveDelta2 (
q,
O3)
;
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 ORDINAL2:sch 2();
A4:
ConsecutiveDelta2 (
q,
O2)
= union (rng L)
by A2, A3, Th20;
assume A5:
O1 c= O2
;
ConsecutiveDelta2 (q,O1) c= ConsecutiveDelta2 (q,O2)
end;
A8:
for O1 being Ordinal st S1[O1] holds
S1[ succ O1]
proof
let O2 be
Ordinal;
( S1[O2] implies S1[ succ O2] )
assume A9:
(
O1 c= O2 implies
ConsecutiveDelta2 (
q,
O1)
c= ConsecutiveDelta2 (
q,
O2) )
;
S1[ succ O2]
assume A10:
O1 c= succ O2
;
ConsecutiveDelta2 (q,O1) c= ConsecutiveDelta2 (q,(succ O2))
per cases
( O1 = succ O2 or O1 <> succ O2 )
;
suppose A11:
O1 <> succ O2
;
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;
verum end;
end;
A13:
S1[ 0 ]
;
for O being Ordinal holds S1[O]
from ORDINAL2:sch 1(A13, A8, A1);
hence
( O1 c= O2 implies ConsecutiveDelta2 (q,O1) c= ConsecutiveDelta2 (q,O2) )
; verum