let A be non empty set ; :: thesis: for L being lower-bounded LATTICE st L is modular holds
for d being BiFunction of A,L st d is symmetric & d is u.t.i. holds
for O being Ordinal
for q being QuadrSeq of d st O c= DistEsti d holds
ConsecutiveDelta2 (q,O) is u.t.i.
let L be lower-bounded LATTICE; :: thesis: ( L is modular implies for d being BiFunction of A,L st d is symmetric & d is u.t.i. holds
for O being Ordinal
for q being QuadrSeq of d st O c= DistEsti d holds
ConsecutiveDelta2 (q,O) is u.t.i. )
assume A1: L is modular ; :: thesis: for d being BiFunction of A,L st d is symmetric & d is u.t.i. holds
for O being Ordinal
for q being QuadrSeq of d st O c= DistEsti d holds
ConsecutiveDelta2 (q,O) is u.t.i.
let d be BiFunction of A,L; :: thesis: ( d is symmetric & d is u.t.i. implies for O being Ordinal
for q being QuadrSeq of d st O c= DistEsti d holds
ConsecutiveDelta2 (q,O) is u.t.i. )
assume that
A2: d is symmetric and
A3: d is u.t.i. ; :: thesis: for O being Ordinal
for q being QuadrSeq of d st O c= DistEsti d holds
ConsecutiveDelta2 (q,O) is u.t.i.
let O be Ordinal; :: thesis: for q being QuadrSeq of d st O c= DistEsti d holds
ConsecutiveDelta2 (q,O) is u.t.i.
let q be QuadrSeq of d; :: thesis: ( O c= DistEsti d implies ConsecutiveDelta2 (q,O) is u.t.i. )
defpred S₁[ Ordinal] means ( $1 c= DistEsti d implies ConsecutiveDelta2 (q,$1) is u.t.i. );
A4: for O1 being Ordinal st S₁[O1] holds
S₁[ succ O1]

proof

let O1 be Ordinal; :: thesis: ( S₁[O1] implies S₁[ succ O1] )
assume that
A5: ( O1 c= DistEsti d implies ConsecutiveDelta2 (q,O1) is u.t.i. ) and
A6: succ O1 c= DistEsti d ; :: thesis: ConsecutiveDelta2 (q,(succ O1)) is u.t.i.
A7: O1 in DistEsti d by A6, ORDINAL1:21;
then A8: O1 in dom q by LATTICE5:25;
then q . O1 in rng q by FUNCT_1:def 3;
then A9: q . O1 in { [u,v,a9,b9] where u, v is Element of A, a9, b9 is Element of L : d . (u,v) <= a9 "\/" b9 } by LATTICE5:def 13;
let x, y, z be Element of ConsecutiveSet2 (A,(succ O1)); :: according to LATTICE5:def 7 :: thesis: (ConsecutiveDelta2 (q,(succ O1))) . (x,z) <= ((ConsecutiveDelta2 (q,(succ O1))) . (x,y)) "\/" ((ConsecutiveDelta2 (q,(succ O1))) . (y,z))
A10: ConsecutiveDelta2 (q,O1) is symmetric by A2, Th26;
reconsider x9 = x, y9 = y, z9 = z as Element of new_set2 (ConsecutiveSet2 (A,O1)) by Th15;
set f = new_bi_fun2 ((ConsecutiveDelta2 (q,O1)),(Quadr2 (q,O1)));
set X = (Quadr2 (q,O1)) `1_4 ;
set Y = (Quadr2 (q,O1)) `2_4 ;
reconsider a = (Quadr2 (q,O1)) `3_4 , b = (Quadr2 (q,O1)) `4_4 as Element of L ;
A11: ( dom d = [:A,A:] & d c= ConsecutiveDelta2 (q,O1) ) by Th23, FUNCT_2:def 1;
consider u, v being Element of A, a9, b9 being Element of L such that
A12: q . O1 = [u,v,a9,b9] and
A13: d . (u,v) <= a9 "\/" b9 by A9;
A14: Quadr2 (q,O1) = [u,v,a9,b9] by A8, A12, Def6;
then A15: ( u = (Quadr2 (q,O1)) `1_4 & v = (Quadr2 (q,O1)) `2_4 ) ;
A16: ( a9 = a & b9 = b ) by A14;
d . (u,v) = d . [u,v]
.= (ConsecutiveDelta2 (q,O1)) . (((Quadr2 (q,O1)) `1_4),((Quadr2 (q,O1)) `2_4)) by A15, A11, GRFUNC_1:2 ;
then new_bi_fun2 ((ConsecutiveDelta2 (q,O1)),(Quadr2 (q,O1))) is u.t.i. by A1, A5, A7, A10, A13, A16, Th12, ORDINAL1:def 2;
then A17: (new_bi_fun2 ((ConsecutiveDelta2 (q,O1)),(Quadr2 (q,O1)))) . (x9,z9) <= ((new_bi_fun2 ((ConsecutiveDelta2 (q,O1)),(Quadr2 (q,O1)))) . (x9,y9)) "\/" ((new_bi_fun2 ((ConsecutiveDelta2 (q,O1)),(Quadr2 (q,O1)))) . (y9,z9)) ;
ConsecutiveDelta2 (q,(succ O1)) = new_bi_fun2 ((BiFun ((ConsecutiveDelta2 (q,O1)),(ConsecutiveSet2 (A,O1)),L)),(Quadr2 (q,O1))) by Th19
.= new_bi_fun2 ((ConsecutiveDelta2 (q,O1)),(Quadr2 (q,O1))) by LATTICE5:def 15 ;
hence (ConsecutiveDelta2 (q,(succ O1))) . (x,z) <= ((ConsecutiveDelta2 (q,(succ O1))) . (x,y)) "\/" ((ConsecutiveDelta2 (q,(succ O1))) . (y,z)) by A17; :: thesis: verum

end;

A18: 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
A19: ( O2 <> 0 & O2 is limit_ordinal ) and
A20: for O1 being Ordinal st O1 in O2 & O1 c= DistEsti d holds
ConsecutiveDelta2 (q,O1) is u.t.i. and
A21: O2 c= DistEsti d ; :: thesis: ConsecutiveDelta2 (q,O2) is u.t.i.
set CS = ConsecutiveSet2 (A,O2);
consider Ls being Sequence such that
A22: ( dom Ls = O2 & ( for O1 being Ordinal st O1 in O2 holds
Ls . O1 = H₁(O1) ) ) from ORDINAL2:sch 2();
ConsecutiveDelta2 (q,O2) = union (rng Ls) by A19, A22, Th20;
then reconsider f = union (rng Ls) as BiFunction of (ConsecutiveSet2 (A,O2)),L ;
deffunc H₂( Ordinal) -> set = ConsecutiveSet2 (A,$1);
consider Ts being Sequence such that
A23: ( dom Ts = O2 & ( for O1 being Ordinal st O1 in O2 holds
Ts . O1 = H₂(O1) ) ) from ORDINAL2:sch 2();
A24: ConsecutiveSet2 (A,O2) = union (rng Ts) by A19, A23, Th16;
f is u.t.i.

proof

let x, y, z be Element of ConsecutiveSet2 (A,O2); :: according to LATTICE5:def 7 :: thesis: f . (x,z) <= (f . (x,y)) "\/" (f . (y,z))
consider X being set such that
A25: x in X and
A26: X in rng Ts by A24, TARSKI:def 4;
consider o1 being object such that
A27: o1 in dom Ts and
A28: X = Ts . o1 by A26, FUNCT_1:def 3;
consider Y being set such that
A29: y in Y and
A30: Y in rng Ts by A24, TARSKI:def 4;
consider o2 being object such that
A31: o2 in dom Ts and
A32: Y = Ts . o2 by A30, FUNCT_1:def 3;
consider Z being set such that
A33: z in Z and
A34: Z in rng Ts by A24, TARSKI:def 4;
consider o3 being object such that
A35: o3 in dom Ts and
A36: Z = Ts . o3 by A34, FUNCT_1:def 3;
reconsider o1 = o1, o2 = o2, o3 = o3 as Ordinal by A27, A31, A35;
A37: x in ConsecutiveSet2 (A,o1) by A23, A25, A27, A28;
A38: Ls . o3 = ConsecutiveDelta2 (q,o3) by A22, A23, A35;
then reconsider h3 = Ls . o3 as BiFunction of (ConsecutiveSet2 (A,o3)),L ;
A39: h3 is u.t.i.

proof

let x, y, z be Element of ConsecutiveSet2 (A,o3); :: according to LATTICE5:def 7 :: thesis: h3 . (x,z) <= (h3 . (x,y)) "\/" (h3 . (y,z))
o3 c= DistEsti d by A21, A23, A35, ORDINAL1:def 2;
then A40: ConsecutiveDelta2 (q,o3) is u.t.i. by A20, A23, A35;
ConsecutiveDelta2 (q,o3) = h3 by A22, A23, A35;
hence h3 . (x,z) <= (h3 . (x,y)) "\/" (h3 . (y,z)) by A40; :: thesis: verum

end;

A41: dom h3 = [:(ConsecutiveSet2 (A,o3)),(ConsecutiveSet2 (A,o3)):] by FUNCT_2:def 1;
A42: z in ConsecutiveSet2 (A,o3) by A23, A33, A35, A36;
A43: Ls . o2 = ConsecutiveDelta2 (q,o2) by A22, A23, A31;
then reconsider h2 = Ls . o2 as BiFunction of (ConsecutiveSet2 (A,o2)),L ;
A44: h2 is u.t.i.

proof

let x, y, z be Element of ConsecutiveSet2 (A,o2); :: according to LATTICE5:def 7 :: thesis: h2 . (x,z) <= (h2 . (x,y)) "\/" (h2 . (y,z))
o2 c= DistEsti d by A21, A23, A31, ORDINAL1:def 2;
then A45: ConsecutiveDelta2 (q,o2) is u.t.i. by A20, A23, A31;
ConsecutiveDelta2 (q,o2) = h2 by A22, A23, A31;
hence h2 . (x,z) <= (h2 . (x,y)) "\/" (h2 . (y,z)) by A45; :: thesis: verum

end;

A46: dom h2 = [:(ConsecutiveSet2 (A,o2)),(ConsecutiveSet2 (A,o2)):] by FUNCT_2:def 1;
A47: Ls . o1 = ConsecutiveDelta2 (q,o1) by A22, A23, A27;
then reconsider h1 = Ls . o1 as BiFunction of (ConsecutiveSet2 (A,o1)),L ;
A48: h1 is u.t.i.

proof

let x, y, z be Element of ConsecutiveSet2 (A,o1); :: according to LATTICE5:def 7 :: thesis: h1 . (x,z) <= (h1 . (x,y)) "\/" (h1 . (y,z))
o1 c= DistEsti d by A21, A23, A27, ORDINAL1:def 2;
then A49: ConsecutiveDelta2 (q,o1) is u.t.i. by A20, A23, A27;
ConsecutiveDelta2 (q,o1) = h1 by A22, A23, A27;
hence h1 . (x,z) <= (h1 . (x,y)) "\/" (h1 . (y,z)) by A49; :: thesis: verum

end;

A50: dom h1 = [:(ConsecutiveSet2 (A,o1)),(ConsecutiveSet2 (A,o1)):] by FUNCT_2:def 1;
A51: y in ConsecutiveSet2 (A,o2) by A23, A29, A31, A32;

per cases ( o1 c= o3 or o3 c= o1 ) ;

suppose A52: o1 c= o3 ; :: thesis: f . (x,z) <= (f . (x,y)) "\/" (f . (y,z))

then A53: ConsecutiveSet2 (A,o1) c= ConsecutiveSet2 (A,o3) by Th21;
thus (f . (x,y)) "\/" (f . (y,z)) >= f . (x,z) :: thesis: verum

proof

per cases ( o2 c= o3 or o3 c= o2 ) ;

suppose A54: o2 c= o3 ; :: thesis: (f . (x,y)) "\/" (f . (y,z)) >= f . (x,z)

reconsider z9 = z as Element of ConsecutiveSet2 (A,o3) by A23, A33, A35, A36;
reconsider x9 = x as Element of ConsecutiveSet2 (A,o3) by A37, A53;
ConsecutiveDelta2 (q,o3) in rng Ls by A22, A23, A35, A38, FUNCT_1:def 3;
then A55: h3 c= f by A38, ZFMISC_1:74;
A56: ConsecutiveSet2 (A,o2) c= ConsecutiveSet2 (A,o3) by A54, Th21;
then reconsider y9 = y as Element of ConsecutiveSet2 (A,o3) by A51;
[y,z] in dom h3 by A51, A42, A41, A56, ZFMISC_1:87;
then A57: f . (y,z) = h3 . (y9,z9) by A55, GRFUNC_1:2;
[x,z] in dom h3 by A37, A42, A41, A53, ZFMISC_1:87;
then A58: f . (x,z) = h3 . (x9,z9) by A55, GRFUNC_1:2;
[x,y] in dom h3 by A37, A51, A41, A53, A56, ZFMISC_1:87;
then f . (x,y) = h3 . (x9,y9) by A55, GRFUNC_1:2;
hence (f . (x,y)) "\/" (f . (y,z)) >= f . (x,z) by A39, A57, A58; :: thesis: verum

end;

suppose A59: o3 c= o2 ; :: thesis: (f . (x,y)) "\/" (f . (y,z)) >= f . (x,z)

reconsider y9 = y as Element of ConsecutiveSet2 (A,o2) by A23, A29, A31, A32;
ConsecutiveDelta2 (q,o2) in rng Ls by A22, A23, A31, A43, FUNCT_1:def 3;
then A60: h2 c= f by A43, ZFMISC_1:74;
A61: ConsecutiveSet2 (A,o3) c= ConsecutiveSet2 (A,o2) by A59, Th21;
then reconsider z9 = z as Element of ConsecutiveSet2 (A,o2) by A42;
[y,z] in dom h2 by A51, A42, A46, A61, ZFMISC_1:87;
then A62: f . (y,z) = h2 . (y9,z9) by A60, GRFUNC_1:2;
ConsecutiveSet2 (A,o1) c= ConsecutiveSet2 (A,o3) by A52, Th21;
then A63: ConsecutiveSet2 (A,o1) c= ConsecutiveSet2 (A,o2) by A61;
then reconsider x9 = x as Element of ConsecutiveSet2 (A,o2) by A37;
[x,y] in dom h2 by A37, A51, A46, A63, ZFMISC_1:87;
then A64: f . (x,y) = h2 . (x9,y9) by A60, GRFUNC_1:2;
[x,z] in dom h2 by A37, A42, A46, A61, A63, ZFMISC_1:87;
then f . (x,z) = h2 . (x9,z9) by A60, GRFUNC_1:2;
hence (f . (x,y)) "\/" (f . (y,z)) >= f . (x,z) by A44, A64, A62; :: thesis: verum

end;

end;

end;

end;

suppose A65: o3 c= o1 ; :: thesis: f . (x,z) <= (f . (x,y)) "\/" (f . (y,z))

then A66: ConsecutiveSet2 (A,o3) c= ConsecutiveSet2 (A,o1) by Th21;
thus (f . (x,y)) "\/" (f . (y,z)) >= f . (x,z) :: thesis: verum

proof

per cases ( o1 c= o2 or o2 c= o1 ) ;

suppose A67: o1 c= o2 ; :: thesis: (f . (x,y)) "\/" (f . (y,z)) >= f . (x,z)

reconsider y9 = y as Element of ConsecutiveSet2 (A,o2) by A23, A29, A31, A32;
ConsecutiveDelta2 (q,o2) in rng Ls by A22, A23, A31, A43, FUNCT_1:def 3;
then A68: h2 c= f by A43, ZFMISC_1:74;
A69: ConsecutiveSet2 (A,o1) c= ConsecutiveSet2 (A,o2) by A67, Th21;
then reconsider x9 = x as Element of ConsecutiveSet2 (A,o2) by A37;
[x,y] in dom h2 by A37, A51, A46, A69, ZFMISC_1:87;
then A70: f . (x,y) = h2 . (x9,y9) by A68, GRFUNC_1:2;
ConsecutiveSet2 (A,o3) c= ConsecutiveSet2 (A,o1) by A65, Th21;
then A71: ConsecutiveSet2 (A,o3) c= ConsecutiveSet2 (A,o2) by A69;
then reconsider z9 = z as Element of ConsecutiveSet2 (A,o2) by A42;
[y,z] in dom h2 by A51, A42, A46, A71, ZFMISC_1:87;
then A72: f . (y,z) = h2 . (y9,z9) by A68, GRFUNC_1:2;
[x,z] in dom h2 by A37, A42, A46, A69, A71, ZFMISC_1:87;
then f . (x,z) = h2 . (x9,z9) by A68, GRFUNC_1:2;
hence (f . (x,y)) "\/" (f . (y,z)) >= f . (x,z) by A44, A70, A72; :: thesis: verum

end;

suppose A73: o2 c= o1 ; :: thesis: (f . (x,y)) "\/" (f . (y,z)) >= f . (x,z)

reconsider x9 = x as Element of ConsecutiveSet2 (A,o1) by A23, A25, A27, A28;
reconsider z9 = z as Element of ConsecutiveSet2 (A,o1) by A42, A66;
ConsecutiveDelta2 (q,o1) in rng Ls by A22, A23, A27, A47, FUNCT_1:def 3;
then A74: h1 c= f by A47, ZFMISC_1:74;
A75: ConsecutiveSet2 (A,o2) c= ConsecutiveSet2 (A,o1) by A73, Th21;
then reconsider y9 = y as Element of ConsecutiveSet2 (A,o1) by A51;
[x,y] in dom h1 by A37, A51, A50, A75, ZFMISC_1:87;
then A76: f . (x,y) = h1 . (x9,y9) by A74, GRFUNC_1:2;
[x,z] in dom h1 by A37, A42, A50, A66, ZFMISC_1:87;
then A77: f . (x,z) = h1 . (x9,z9) by A74, GRFUNC_1:2;
[y,z] in dom h1 by A51, A42, A50, A66, A75, ZFMISC_1:87;
then f . (y,z) = h1 . (y9,z9) by A74, GRFUNC_1:2;
hence (f . (x,y)) "\/" (f . (y,z)) >= f . (x,z) by A48, A76, A77; :: thesis: verum

end;

end;

end;

end;

end;

end;

hence ConsecutiveDelta2 (q,O2) is u.t.i. by A19, A22, Th20; :: thesis: verum

end;

A78: S₁[ 0 ]

proof

assume 0 c= DistEsti d ; :: thesis: ConsecutiveDelta2 (q,0) is u.t.i.
let x, y, z be Element of ConsecutiveSet2 (A,0); :: according to LATTICE5:def 7 :: thesis: (ConsecutiveDelta2 (q,0)) . (x,z) <= ((ConsecutiveDelta2 (q,0)) . (x,y)) "\/" ((ConsecutiveDelta2 (q,0)) . (y,z))
reconsider x9 = x, y9 = y, z9 = z as Element of A by Th14;
( ConsecutiveDelta2 (q,0) = d & d . (x9,z9) <= (d . (x9,y9)) "\/" (d . (y9,z9)) ) by A3, Th18;
hence (ConsecutiveDelta2 (q,0)) . (x,z) <= ((ConsecutiveDelta2 (q,0)) . (x,y)) "\/" ((ConsecutiveDelta2 (q,0)) . (y,z)) ; :: thesis: verum

end;

for O being Ordinal holds S₁[O] from ORDINAL2:sch 1(A78, A4, A18);
hence ( O c= DistEsti d implies ConsecutiveDelta2 (q,O) is u.t.i. ) ; :: thesis: verum