let A be non empty set ; :: thesis: for L being lower-bounded LATTICE
for O being Ordinal
for d being BiFunction of A,L st d is symmetric & d is u.t.i. holds
for q being QuadrSeq of d st O c= DistEsti d holds
ConsecutiveDelta (q,O) is u.t.i.
let L be lower-bounded LATTICE; :: thesis: for O being Ordinal
for d being BiFunction of A,L st d is symmetric & d is u.t.i. holds
for q being QuadrSeq of d st O c= DistEsti d holds
ConsecutiveDelta (q,O) is u.t.i.
let O be Ordinal; :: thesis: for d being BiFunction of A,L st d is symmetric & d is u.t.i. holds
for q being QuadrSeq of d st O c= DistEsti d holds
ConsecutiveDelta (q,O) is u.t.i.
let d be BiFunction of A,L; :: thesis: ( d is symmetric & d is u.t.i. implies for q being QuadrSeq of d st O c= DistEsti d holds
ConsecutiveDelta (q,O) is u.t.i. )
assume that
A1: d is symmetric and
A2: d is u.t.i. ; :: thesis: for q being QuadrSeq of d st O c= DistEsti d holds
ConsecutiveDelta (q,O) is u.t.i.
let q be QuadrSeq of d; :: thesis: ( O c= DistEsti d implies ConsecutiveDelta (q,O) is u.t.i. )
defpred S₁[ Ordinal] means ( $1 c= DistEsti d implies ConsecutiveDelta (q,$1) is u.t.i. );
A3: 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
A4: ( O1 c= DistEsti d implies ConsecutiveDelta (q,O1) is u.t.i. ) and
A5: succ O1 c= DistEsti d ; :: thesis: ConsecutiveDelta (q,(succ O1)) is u.t.i.
A6: O1 in DistEsti d by A5, ORDINAL1:21;
then A7: O1 in dom q by Th25;
then q . O1 in rng q by FUNCT_1:def 3;
then A8: 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 Def13;
let x, y, z be Element of ConsecutiveSet (A,(succ O1)); :: according to LATTICE5:def 7 :: thesis: ((ConsecutiveDelta (q,(succ O1))) . (x,y)) "\/" ((ConsecutiveDelta (q,(succ O1))) . (y,z)) >= (ConsecutiveDelta (q,(succ O1))) . (x,z)
A9: ConsecutiveDelta (q,O1) is symmetric by A1, Th34;
reconsider x9 = x, y9 = y, z9 = z as Element of new_set (ConsecutiveSet (A,O1)) by Th22;
set f = new_bi_fun ((ConsecutiveDelta (q,O1)),(Quadr (q,O1)));
set X = (Quadr (q,O1)) `1_4 ;
set Y = (Quadr (q,O1)) `2_4 ;
reconsider a = (Quadr (q,O1)) `3_4 , b = (Quadr (q,O1)) `4_4 as Element of L ;
A10: ( dom d = [:A,A:] & d c= ConsecutiveDelta (q,O1) ) by Th31, FUNCT_2:def 1;
consider u, v being Element of A, a9, b9 being Element of L such that
A11: q . O1 = [u,v,a9,b9] and
A12: d . (u,v) <= a9 "\/" b9 by A8;
A13: Quadr (q,O1) = [u,v,a9,b9] by A7, A11, Def14;
then A14: ( u = (Quadr (q,O1)) `1_4 & v = (Quadr (q,O1)) `2_4 ) ;
A15: ( a9 = a & b9 = b ) by A13;
d . (u,v) = d . [u,v]
.= (ConsecutiveDelta (q,O1)) . (((Quadr (q,O1)) `1_4),((Quadr (q,O1)) `2_4)) by A14, A10, GRFUNC_1:2 ;
then new_bi_fun ((ConsecutiveDelta (q,O1)),(Quadr (q,O1))) is u.t.i. by A4, A6, A9, A12, A15, Th18, ORDINAL1:def 2;
then A16: (new_bi_fun ((ConsecutiveDelta (q,O1)),(Quadr (q,O1)))) . (x9,z9) <= ((new_bi_fun ((ConsecutiveDelta (q,O1)),(Quadr (q,O1)))) . (x9,y9)) "\/" ((new_bi_fun ((ConsecutiveDelta (q,O1)),(Quadr (q,O1)))) . (y9,z9)) ;
ConsecutiveDelta (q,(succ O1)) = new_bi_fun ((BiFun ((ConsecutiveDelta (q,O1)),(ConsecutiveSet (A,O1)),L)),(Quadr (q,O1))) by Th27
.= new_bi_fun ((ConsecutiveDelta (q,O1)),(Quadr (q,O1))) by Def15 ;
hence (ConsecutiveDelta (q,(succ O1))) . (x,z) <= ((ConsecutiveDelta (q,(succ O1))) . (x,y)) "\/" ((ConsecutiveDelta (q,(succ O1))) . (y,z)) by A16; :: thesis: verum

end;

A17: for O2 being Ordinal st O2 <> 0 & O2 is limit_ordinal & ( for O1 being Ordinal st O1 in O2 holds
S₁[O1] ) holds
S₁[O2]

proof

deffunc H₁( Ordinal) -> BiFunction of (ConsecutiveSet (A,$1)),L = ConsecutiveDelta (q,$1);
let O2 be Ordinal; :: thesis: ( O2 <> 0 & O2 is limit_ordinal & ( for O1 being Ordinal st O1 in O2 holds
S₁[O1] ) implies S₁[O2] )
assume that
A18: ( O2 <> 0 & O2 is limit_ordinal ) and
A19: for O1 being Ordinal st O1 in O2 & O1 c= DistEsti d holds
ConsecutiveDelta (q,O1) is u.t.i. and
A20: O2 c= DistEsti d ; :: thesis: ConsecutiveDelta (q,O2) is u.t.i.
set CS = ConsecutiveSet (A,O2);
consider Ls being Sequence such that
A21: ( dom Ls = O2 & ( for O1 being Ordinal st O1 in O2 holds
Ls . O1 = H₁(O1) ) ) from ORDINAL2:sch 2();
ConsecutiveDelta (q,O2) = union (rng Ls) by A18, A21, Th28;
then reconsider f = union (rng Ls) as BiFunction of (ConsecutiveSet (A,O2)),L ;
deffunc H₂( Ordinal) -> set = ConsecutiveSet (A,$1);
consider Ts being Sequence such that
A22: ( dom Ts = O2 & ( for O1 being Ordinal st O1 in O2 holds
Ts . O1 = H₂(O1) ) ) from ORDINAL2:sch 2();
A23: ConsecutiveSet (A,O2) = union (rng Ts) by A18, A22, Th23;
f is u.t.i.

proof

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

proof

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

end;

A40: dom h3 = [:(ConsecutiveSet (A,o3)),(ConsecutiveSet (A,o3)):] by FUNCT_2:def 1;
A41: z in ConsecutiveSet (A,o3) by A22, A32, A34, A35;
A42: Ls . o2 = ConsecutiveDelta (q,o2) by A21, A22, A30;
then reconsider h2 = Ls . o2 as BiFunction of (ConsecutiveSet (A,o2)),L ;
A43: h2 is u.t.i.

proof

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

end;

A45: dom h2 = [:(ConsecutiveSet (A,o2)),(ConsecutiveSet (A,o2)):] by FUNCT_2:def 1;
A46: Ls . o1 = ConsecutiveDelta (q,o1) by A21, A22, A26;
then reconsider h1 = Ls . o1 as BiFunction of (ConsecutiveSet (A,o1)),L ;
A47: h1 is u.t.i.

proof

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

end;

A49: dom h1 = [:(ConsecutiveSet (A,o1)),(ConsecutiveSet (A,o1)):] by FUNCT_2:def 1;
A50: y in ConsecutiveSet (A,o2) by A22, A28, A30, A31;

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

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

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

proof

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

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

reconsider z9 = z as Element of ConsecutiveSet (A,o3) by A22, A32, A34, A35;
reconsider x9 = x as Element of ConsecutiveSet (A,o3) by A36, A52;
ConsecutiveDelta (q,o3) in rng Ls by A21, A22, A34, A37, FUNCT_1:def 3;
then A54: h3 c= f by A37, ZFMISC_1:74;
A55: ConsecutiveSet (A,o2) c= ConsecutiveSet (A,o3) by A53, Th29;
then reconsider y9 = y as Element of ConsecutiveSet (A,o3) by A50;
[y,z] in dom h3 by A50, A41, A40, A55, ZFMISC_1:87;
then A56: f . (y,z) = h3 . (y9,z9) by A54, GRFUNC_1:2;
[x,z] in dom h3 by A36, A41, A40, A52, ZFMISC_1:87;
then A57: f . (x,z) = h3 . (x9,z9) by A54, GRFUNC_1:2;
[x,y] in dom h3 by A36, A50, A40, A52, A55, ZFMISC_1:87;
then f . (x,y) = h3 . (x9,y9) by A54, GRFUNC_1:2;
hence (f . (x,y)) "\/" (f . (y,z)) >= f . (x,z) by A38, A56, A57; :: thesis: verum

end;

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

reconsider y9 = y as Element of ConsecutiveSet (A,o2) by A22, A28, A30, A31;
ConsecutiveDelta (q,o2) in rng Ls by A21, A22, A30, A42, FUNCT_1:def 3;
then A59: h2 c= f by A42, ZFMISC_1:74;
A60: ConsecutiveSet (A,o3) c= ConsecutiveSet (A,o2) by A58, Th29;
then reconsider z9 = z as Element of ConsecutiveSet (A,o2) by A41;
[y,z] in dom h2 by A50, A41, A45, A60, ZFMISC_1:87;
then A61: f . (y,z) = h2 . (y9,z9) by A59, GRFUNC_1:2;
ConsecutiveSet (A,o1) c= ConsecutiveSet (A,o3) by A51, Th29;
then A62: ConsecutiveSet (A,o1) c= ConsecutiveSet (A,o2) by A60;
then reconsider x9 = x as Element of ConsecutiveSet (A,o2) by A36;
[x,y] in dom h2 by A36, A50, A45, A62, ZFMISC_1:87;
then A63: f . (x,y) = h2 . (x9,y9) by A59, GRFUNC_1:2;
[x,z] in dom h2 by A36, A41, A45, A60, A62, ZFMISC_1:87;
then f . (x,z) = h2 . (x9,z9) by A59, GRFUNC_1:2;
hence (f . (x,y)) "\/" (f . (y,z)) >= f . (x,z) by A43, A63, A61; :: thesis: verum

end;

end;

end;

end;

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

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

proof

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

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

reconsider y9 = y as Element of ConsecutiveSet (A,o2) by A22, A28, A30, A31;
ConsecutiveDelta (q,o2) in rng Ls by A21, A22, A30, A42, FUNCT_1:def 3;
then A67: h2 c= f by A42, ZFMISC_1:74;
A68: ConsecutiveSet (A,o1) c= ConsecutiveSet (A,o2) by A66, Th29;
then reconsider x9 = x as Element of ConsecutiveSet (A,o2) by A36;
[x,y] in dom h2 by A36, A50, A45, A68, ZFMISC_1:87;
then A69: f . (x,y) = h2 . (x9,y9) by A67, GRFUNC_1:2;
ConsecutiveSet (A,o3) c= ConsecutiveSet (A,o1) by A64, Th29;
then A70: ConsecutiveSet (A,o3) c= ConsecutiveSet (A,o2) by A68;
then reconsider z9 = z as Element of ConsecutiveSet (A,o2) by A41;
[y,z] in dom h2 by A50, A41, A45, A70, ZFMISC_1:87;
then A71: f . (y,z) = h2 . (y9,z9) by A67, GRFUNC_1:2;
[x,z] in dom h2 by A36, A41, A45, A68, A70, ZFMISC_1:87;
then f . (x,z) = h2 . (x9,z9) by A67, GRFUNC_1:2;
hence (f . (x,y)) "\/" (f . (y,z)) >= f . (x,z) by A43, A69, A71; :: thesis: verum

end;

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

reconsider x9 = x as Element of ConsecutiveSet (A,o1) by A22, A24, A26, A27;
reconsider z9 = z as Element of ConsecutiveSet (A,o1) by A41, A65;
ConsecutiveDelta (q,o1) in rng Ls by A21, A22, A26, A46, FUNCT_1:def 3;
then A73: h1 c= f by A46, ZFMISC_1:74;
A74: ConsecutiveSet (A,o2) c= ConsecutiveSet (A,o1) by A72, Th29;
then reconsider y9 = y as Element of ConsecutiveSet (A,o1) by A50;
[x,y] in dom h1 by A36, A50, A49, A74, ZFMISC_1:87;
then A75: f . (x,y) = h1 . (x9,y9) by A73, GRFUNC_1:2;
[x,z] in dom h1 by A36, A41, A49, A65, ZFMISC_1:87;
then A76: f . (x,z) = h1 . (x9,z9) by A73, GRFUNC_1:2;
[y,z] in dom h1 by A50, A41, A49, A65, A74, ZFMISC_1:87;
then f . (y,z) = h1 . (y9,z9) by A73, GRFUNC_1:2;
hence (f . (x,y)) "\/" (f . (y,z)) >= f . (x,z) by A47, A75, A76; :: thesis: verum

end;

end;

end;

end;

end;

end;

hence ConsecutiveDelta (q,O2) is u.t.i. by A18, A21, Th28; :: thesis: verum

end;

A77: S₁[ 0 ]

proof

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

end;

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