:: J\'onsson Theorem
:: by Jaros{\l}aw Gryko
::
:: Received November 13, 1997
:: Copyright (c) 1997 Association of Mizar Users


theorem Th1: :: LATTICE5:1
for f being Function
for F being Function-yielding Function st f = union (rng F) holds
dom f = union (rng (doms F))
proof end;

theorem Th2: :: LATTICE5:2
for A, B being non empty set holds [:(union A),(union B):] = union { [:a,b:] where a is Element of A, b is Element of B : ( a in A & b in B ) }
proof end;

theorem Th3: :: LATTICE5:3
for A being non empty set st A is c=-linear holds
[:(union A),(union A):] = union { [:a,a:] where a is Element of A : a in A }
proof end;

definition
let A be set ;
func EqRelLATT A -> Poset equals :: LATTICE5:def 1
 LattPOSet (EqRelLatt A);
correctness
coherence
LattPOSet (EqRelLatt A) is Poset;
;
end;

:: deftheorem defines EqRelLATT LATTICE5:def 1 :
for A being set holds EqRelLATT A = LattPOSet (EqRelLatt A);

registration
let A be set ;
cluster EqRelLATT A -> with_suprema with_infima ;
coherence
( EqRelLATT A is with_infima & EqRelLATT A is with_suprema ) ;
end;

theorem Th4: :: LATTICE5:4
for A, x being set holds
( x in the carrier of (EqRelLATT A) iff x is Equivalence_Relation of A )
proof end;

theorem Th5: :: LATTICE5:5
for A being set
for x, y being Element of (EqRelLatt A) holds
( x [= y iff x c= y )
proof end;

theorem Th6: :: LATTICE5:6
for A being set
for a, b being Element of (EqRelLATT A) holds
( a <= b iff a c= b )
proof end;

theorem Th7: :: LATTICE5:7
for L being Lattice
for a, b being Element of (LattPOSet L) holds a "/\" b = (% a) "/\" (% b)
proof end;

theorem Th8: :: LATTICE5:8
for A being set
for a, b being Element of (EqRelLATT A) holds a "/\" b = a /\ b
proof end;

theorem Th9: :: LATTICE5:9
for L being Lattice
for a, b being Element of (LattPOSet L) holds a "\/" b = (% a) "\/" (% b)
proof end;

theorem Th10: :: LATTICE5:10
for A being set
for a, b being Element of (EqRelLATT A)
for E1, E2 being Equivalence_Relation of A st a = E1 & b = E2 holds
a "\/" b = E1 "\/" E2
proof end;

definition
let L be non empty RelStr ;
redefine attr L is complete means :: LATTICE5:def 2
for X being Subset of L ex a being Element of L st
( a is_<=_than X & ( for b being Element of L st b is_<=_than X holds
b <= a ) );
compatibility
( L is complete iff for X being Subset of L ex a being Element of L st
( a is_<=_than X & ( for b being Element of L st b is_<=_than X holds
b <= a ) ) )
proof end;
end;

:: deftheorem defines complete LATTICE5:def 2 :
for L being non empty RelStr holds
( L is complete iff for X being Subset of L ex a being Element of L st
( a is_<=_than X & ( for b being Element of L st b is_<=_than X holds
b <= a ) ) );

registration
let A be set ;
cluster EqRelLATT A -> complete ;
coherence
EqRelLATT A is complete
proof end;
end;

registration
let L1, L2 be LATTICE;
cluster meet-preserving join-preserving Relation of the carrier of L1,the carrier of L2;
existence
ex b1 being Function of L1,L2 st
( b1 is meet-preserving & b1 is join-preserving )
proof end;
end;

definition
let L1, L2 be LATTICE;
mode Homomorphism of L1,L2 is meet-preserving join-preserving Function of L1,L2;
end;

registration
let L be LATTICE;
cluster strict meet-inheriting join-inheriting SubRelStr of L;
existence
ex b1 being SubRelStr of L st
( b1 is meet-inheriting & b1 is join-inheriting & b1 is strict )
proof end;
end;

definition
let L be non empty RelStr ;
mode Sublattice of L is meet-inheriting join-inheriting SubRelStr of L;
end;

definition
let L1, L2 be LATTICE;
let f be Homomorphism of L1,L2;
:: original: Image
redefine func Image f -> strict full Sublattice of L2;
coherence
Image f is strict full Sublattice of L2
proof end;
end;

definition
let X be non empty set ;
let f be non empty FinSequence of X;
let x, y be set ;
let R1, R2 be Relation;
pred x,y are_joint_by f,R1,R2 means :Def3: :: LATTICE5:def 3
( f . 1 = x & f . (len f) = y & ( for i being Element of NAT st 1 <= i & i < len f holds
( ( not i is even implies [(f . i),(f . (i + 1))] in R1 ) & ( i is even implies [(f . i),(f . (i + 1))] in R2 ) ) ) );
end;

:: deftheorem Def3 defines are_joint_by LATTICE5:def 3 :
for X being non empty set
for f being non empty FinSequence of X
for x, y being set
for R1, R2 being Relation holds
( x,y are_joint_by f,R1,R2 iff ( f . 1 = x & f . (len f) = y & ( for i being Element of NAT st 1 <= i & i < len f holds
( ( not i is even implies [(f . i),(f . (i + 1))] in R1 ) & ( i is even implies [(f . i),(f . (i + 1))] in R2 ) ) ) ) );

theorem :: LATTICE5:11
canceled;

theorem Th12: :: LATTICE5:12
for X being non empty set
for x being set
for o being Element of NAT
for R1, R2 being Relation
for f being non empty FinSequence of X st R1 is_reflexive_in X & R2 is_reflexive_in X & f = o |-> x holds
x,x are_joint_by f,R1,R2
proof end;

Lm1: now
let i, n, m be Element of NAT ; :: thesis: ( 1 <= i & i < n + m & not ( 1 <= i & i < n ) & not ( n = i & i < n + m ) implies ( n + 1 <= i & i < n + m ) )
assume ( 1 <= i & i < n + m ) ; :: thesis: ( ( 1 <= i & i < n ) or ( n = i & i < n + m ) or ( n + 1 <= i & i < n + m ) )
then ( ( 1 <= i & i < n ) or ( n = i & i < n + m ) or ( n < i & i < n + m ) ) by XXREAL_0:1;
hence ( ( 1 <= i & i < n ) or ( n = i & i < n + m ) or ( n + 1 <= i & i < n + m ) ) by NAT_1:13; :: thesis: verum
end;

theorem :: LATTICE5:13
canceled;

theorem Th14: :: LATTICE5:14
for X being non empty set
for x, y being set
for R1, R2 being Relation
for n, m being Element of NAT st n <= m & R1 is_reflexive_in X & R2 is_reflexive_in X & ex f being non empty FinSequence of X st
( len f = n & x,y are_joint_by f,R1,R2 ) holds
ex h being non empty FinSequence of X st
( len h = m & x,y are_joint_by h,R1,R2 )
proof end;

definition
let X be non empty set ;
let Y be Sublattice of EqRelLATT X;
given e being Equivalence_Relation of X such that A1: e in the carrier of Y and
A2: e <> id X ;
given o being Element of NAT such that A3: for e1, e2 being Equivalence_Relation of X
for x, y being set st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds
ex F being non empty FinSequence of X st
( len F = o & x,y are_joint_by F,e1,e2 ) ;
func type_of Y -> Element of NAT means :Def4: :: LATTICE5:def 4
( ( for e1, e2 being Equivalence_Relation of X
for x, y being set st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds
ex F being non empty FinSequence of X st
( len F = it + 2 & x,y are_joint_by F,e1,e2 ) ) & ex e1, e2 being Equivalence_Relation of X ex x, y being set st
( e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 & ( for F being non empty FinSequence of X holds
( not len F = it + 1 or not x,y are_joint_by F,e1,e2 ) ) ) );
existence
ex b1 being Element of NAT st
( ( for e1, e2 being Equivalence_Relation of X
for x, y being set st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds
ex F being non empty FinSequence of X st
( len F = b1 + 2 & x,y are_joint_by F,e1,e2 ) ) & ex e1, e2 being Equivalence_Relation of X ex x, y being set st
( e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 & ( for F being non empty FinSequence of X holds
( not len F = b1 + 1 or not x,y are_joint_by F,e1,e2 ) ) ) )
proof end;
uniqueness
for b1, b2 being Element of NAT st ( for e1, e2 being Equivalence_Relation of X
for x, y being set st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds
ex F being non empty FinSequence of X st
( len F = b1 + 2 & x,y are_joint_by F,e1,e2 ) ) & ex e1, e2 being Equivalence_Relation of X ex x, y being set st
( e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 & ( for F being non empty FinSequence of X holds
( not len F = b1 + 1 or not x,y are_joint_by F,e1,e2 ) ) ) & ( for e1, e2 being Equivalence_Relation of X
for x, y being set st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds
ex F being non empty FinSequence of X st
( len F = b2 + 2 & x,y are_joint_by F,e1,e2 ) ) & ex e1, e2 being Equivalence_Relation of X ex x, y being set st
( e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 & ( for F being non empty FinSequence of X holds
( not len F = b2 + 1 or not x,y are_joint_by F,e1,e2 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines type_of LATTICE5:def 4 :
for X being non empty set
for Y being Sublattice of EqRelLATT X st ex e being Equivalence_Relation of X st
( e in the carrier of Y & e <> id X ) & ex o being Element of NAT st
for e1, e2 being Equivalence_Relation of X
for x, y being set st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds
ex F being non empty FinSequence of X st
( len F = o & x,y are_joint_by F,e1,e2 ) holds
for b3 being Element of NAT holds
( b3 = type_of Y iff ( ( for e1, e2 being Equivalence_Relation of X
for x, y being set st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds
ex F being non empty FinSequence of X st
( len F = b3 + 2 & x,y are_joint_by F,e1,e2 ) ) & ex e1, e2 being Equivalence_Relation of X ex x, y being set st
( e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 & ( for F being non empty FinSequence of X holds
( not len F = b3 + 1 or not x,y are_joint_by F,e1,e2 ) ) ) ) );

theorem Th15: :: LATTICE5:15
for X being non empty set
for Y being Sublattice of EqRelLATT X
for n being Element of NAT st ex e being Equivalence_Relation of X st
( e in the carrier of Y & e <> id X ) & ( for e1, e2 being Equivalence_Relation of X
for x, y being set st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds
ex F being non empty FinSequence of X st
( len F = n + 2 & x,y are_joint_by F,e1,e2 ) ) holds
type_of Y <= n
proof end;

definition
let A be set ;
let L be 1-sorted ;
mode BiFunction of A,L is Function of [:A,A:],the carrier of L;
end;

definition
let A be non empty set ;
let L be 1-sorted ;
let f be BiFunction of A,L;
let x, y be Element of A;
:: original: .
redefine func f . x,y -> Element of L;
coherence
f . x,y is Element of L
proof end;
end;

definition
let A be non empty set ;
let L be 1-sorted ;
let f be BiFunction of A,L;
canceled;
attr f is symmetric means :Def6: :: LATTICE5:def 6
for x, y being Element of A holds f . x,y = f . y,x;
end;

:: deftheorem LATTICE5:def 5 :
canceled;

:: deftheorem Def6 defines symmetric LATTICE5:def 6 :
for A being non empty set
for L being 1-sorted
for f being BiFunction of A,L holds
( f is symmetric iff for x, y being Element of A holds f . x,y = f . y,x );

definition
let A be non empty set ;
let L be lower-bounded LATTICE;
let f be BiFunction of A,L;
attr f is zeroed means :Def7: :: LATTICE5:def 7
for x being Element of A holds f . x,x = Bottom L;
attr f is u.t.i. means :Def8: :: LATTICE5:def 8
for x, y, z being Element of A holds (f . x,y) "\/" (f . y,z) >= f . x,z;
end;

:: deftheorem Def7 defines zeroed LATTICE5:def 7 :
for A being non empty set
for L being lower-bounded LATTICE
for f being BiFunction of A,L holds
( f is zeroed iff for x being Element of A holds f . x,x = Bottom L );

:: deftheorem Def8 defines u.t.i. LATTICE5:def 8 :
for A being non empty set
for L being lower-bounded LATTICE
for f being BiFunction of A,L holds
( f is u.t.i. iff for x, y, z being Element of A holds (f . x,y) "\/" (f . y,z) >= f . x,z );

registration
let A be non empty set ;
let L be lower-bounded LATTICE;
cluster symmetric zeroed u.t.i. Relation of [:A,A:],the carrier of L;
existence
ex b1 being BiFunction of A,L st
( b1 is symmetric & b1 is zeroed & b1 is u.t.i. )
proof end;
end;

definition
let A be non empty set ;
let L be lower-bounded LATTICE;
mode distance_function of A,L is symmetric zeroed u.t.i. BiFunction of A,L;
end;

definition
let A be non empty set ;
let L be lower-bounded LATTICE;
let d be distance_function of A,L;
func alpha d -> Function of L,(EqRelLATT A) means :Def9: :: LATTICE5:def 9
for e being Element of L ex E being Equivalence_Relation of A st
( E = it . e & ( for x, y being Element of A holds
( [x,y] in E iff d . x,y <= e ) ) );
existence
ex b1 being Function of L,(EqRelLATT A) st
for e being Element of L ex E being Equivalence_Relation of A st
( E = b1 . e & ( for x, y being Element of A holds
( [x,y] in E iff d . x,y <= e ) ) )
proof end;
uniqueness
for b1, b2 being Function of L,(EqRelLATT A) st ( for e being Element of L ex E being Equivalence_Relation of A st
( E = b1 . e & ( for x, y being Element of A holds
( [x,y] in E iff d . x,y <= e ) ) ) ) & ( for e being Element of L ex E being Equivalence_Relation of A st
( E = b2 . e & ( for x, y being Element of A holds
( [x,y] in E iff d . x,y <= e ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines alpha LATTICE5:def 9 :
for A being non empty set
for L being lower-bounded LATTICE
for d being distance_function of A,L
for b4 being Function of L,(EqRelLATT A) holds
( b4 = alpha d iff for e being Element of L ex E being Equivalence_Relation of A st
( E = b4 . e & ( for x, y being Element of A holds
( [x,y] in E iff d . x,y <= e ) ) ) );

theorem Th16: :: LATTICE5:16
for A being non empty set
for L being lower-bounded LATTICE
for d being distance_function of A,L holds alpha d is meet-preserving
proof end;

theorem Th17: :: LATTICE5:17
for A being non empty set
for L being lower-bounded LATTICE
for d being distance_function of A,L st d is onto holds
alpha d is one-to-one
proof end;

definition
let A be set ;
func new_set A -> set equals :: LATTICE5:def 10
A \/ {{A},{{A}},{{{A}}}};
correctness
coherence
A \/ {{A},{{A}},{{{A}}}} is set ;
;
end;

:: deftheorem defines new_set LATTICE5:def 10 :
for A being set holds new_set A = A \/ {{A},{{A}},{{{A}}}};

registration
let A be set ;
cluster new_set A -> non empty ;
coherence
not new_set A is empty ;
end;

definition
let A be non empty set ;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
let q be Element of [:A,A,the carrier of L,the carrier of L:];
func new_bi_fun d,q -> BiFunction of (new_set A),L means :Def11: :: LATTICE5:def 11
( ( for u, v being Element of A holds it . u,v = d . u,v ) & it . {A},{A} = Bottom L & it . {{A}},{{A}} = Bottom L & it . {{{A}}},{{{A}}} = Bottom L & it . {{A}},{{{A}}} = q `3 & it . {{{A}}},{{A}} = q `3 & it . {A},{{A}} = q `4 & it . {{A}},{A} = q `4 & it . {A},{{{A}}} = (q `3 ) "\/" (q `4 ) & it . {{{A}}},{A} = (q `3 ) "\/" (q `4 ) & ( for u being Element of A holds
( it . u,{A} = (d . u,(q `1 )) "\/" (q `3 ) & it . {A},u = (d . u,(q `1 )) "\/" (q `3 ) & it . u,{{A}} = ((d . u,(q `1 )) "\/" (q `3 )) "\/" (q `4 ) & it . {{A}},u = ((d . u,(q `1 )) "\/" (q `3 )) "\/" (q `4 ) & it . u,{{{A}}} = (d . u,(q `2 )) "\/" (q `4 ) & it . {{{A}}},u = (d . u,(q `2 )) "\/" (q `4 ) ) ) );
existence
ex b1 being BiFunction of (new_set A),L st
( ( for u, v being Element of A holds b1 . u,v = d . u,v ) & b1 . {A},{A} = Bottom L & b1 . {{A}},{{A}} = Bottom L & b1 . {{{A}}},{{{A}}} = Bottom L & b1 . {{A}},{{{A}}} = q `3 & b1 . {{{A}}},{{A}} = q `3 & b1 . {A},{{A}} = q `4 & b1 . {{A}},{A} = q `4 & b1 . {A},{{{A}}} = (q `3 ) "\/" (q `4 ) & b1 . {{{A}}},{A} = (q `3 ) "\/" (q `4 ) & ( for u being Element of A holds
( b1 . u,{A} = (d . u,(q `1 )) "\/" (q `3 ) & b1 . {A},u = (d . u,(q `1 )) "\/" (q `3 ) & b1 . u,{{A}} = ((d . u,(q `1 )) "\/" (q `3 )) "\/" (q `4 ) & b1 . {{A}},u = ((d . u,(q `1 )) "\/" (q `3 )) "\/" (q `4 ) & b1 . u,{{{A}}} = (d . u,(q `2 )) "\/" (q `4 ) & b1 . {{{A}}},u = (d . u,(q `2 )) "\/" (q `4 ) ) ) )
proof end;
uniqueness
for b1, b2 being BiFunction of (new_set A),L st ( for u, v being Element of A holds b1 . u,v = d . u,v ) & b1 . {A},{A} = Bottom L & b1 . {{A}},{{A}} = Bottom L & b1 . {{{A}}},{{{A}}} = Bottom L & b1 . {{A}},{{{A}}} = q `3 & b1 . {{{A}}},{{A}} = q `3 & b1 . {A},{{A}} = q `4 & b1 . {{A}},{A} = q `4 & b1 . {A},{{{A}}} = (q `3 ) "\/" (q `4 ) & b1 . {{{A}}},{A} = (q `3 ) "\/" (q `4 ) & ( for u being Element of A holds
( b1 . u,{A} = (d . u,(q `1 )) "\/" (q `3 ) & b1 . {A},u = (d . u,(q `1 )) "\/" (q `3 ) & b1 . u,{{A}} = ((d . u,(q `1 )) "\/" (q `3 )) "\/" (q `4 ) & b1 . {{A}},u = ((d . u,(q `1 )) "\/" (q `3 )) "\/" (q `4 ) & b1 . u,{{{A}}} = (d . u,(q `2 )) "\/" (q `4 ) & b1 . {{{A}}},u = (d . u,(q `2 )) "\/" (q `4 ) ) ) & ( for u, v being Element of A holds b2 . u,v = d . u,v ) & b2 . {A},{A} = Bottom L & b2 . {{A}},{{A}} = Bottom L & b2 . {{{A}}},{{{A}}} = Bottom L & b2 . {{A}},{{{A}}} = q `3 & b2 . {{{A}}},{{A}} = q `3 & b2 . {A},{{A}} = q `4 & b2 . {{A}},{A} = q `4 & b2 . {A},{{{A}}} = (q `3 ) "\/" (q `4 ) & b2 . {{{A}}},{A} = (q `3 ) "\/" (q `4 ) & ( for u being Element of A holds
( b2 . u,{A} = (d . u,(q `1 )) "\/" (q `3 ) & b2 . {A},u = (d . u,(q `1 )) "\/" (q `3 ) & b2 . u,{{A}} = ((d . u,(q `1 )) "\/" (q `3 )) "\/" (q `4 ) & b2 . {{A}},u = ((d . u,(q `1 )) "\/" (q `3 )) "\/" (q `4 ) & b2 . u,{{{A}}} = (d . u,(q `2 )) "\/" (q `4 ) & b2 . {{{A}}},u = (d . u,(q `2 )) "\/" (q `4 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines new_bi_fun LATTICE5:def 11 :
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for q being Element of [:A,A,the carrier of L,the carrier of L:]
for b5 being BiFunction of (new_set A),L holds
( b5 = new_bi_fun d,q iff ( ( for u, v being Element of A holds b5 . u,v = d . u,v ) & b5 . {A},{A} = Bottom L & b5 . {{A}},{{A}} = Bottom L & b5 . {{{A}}},{{{A}}} = Bottom L & b5 . {{A}},{{{A}}} = q `3 & b5 . {{{A}}},{{A}} = q `3 & b5 . {A},{{A}} = q `4 & b5 . {{A}},{A} = q `4 & b5 . {A},{{{A}}} = (q `3 ) "\/" (q `4 ) & b5 . {{{A}}},{A} = (q `3 ) "\/" (q `4 ) & ( for u being Element of A holds
( b5 . u,{A} = (d . u,(q `1 )) "\/" (q `3 ) & b5 . {A},u = (d . u,(q `1 )) "\/" (q `3 ) & b5 . u,{{A}} = ((d . u,(q `1 )) "\/" (q `3 )) "\/" (q `4 ) & b5 . {{A}},u = ((d . u,(q `1 )) "\/" (q `3 )) "\/" (q `4 ) & b5 . u,{{{A}}} = (d . u,(q `2 )) "\/" (q `4 ) & b5 . {{{A}}},u = (d . u,(q `2 )) "\/" (q `4 ) ) ) ) );

theorem Th18: :: LATTICE5:18
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L st d is zeroed holds
for q being Element of [:A,A,the carrier of L,the carrier of L:] holds new_bi_fun d,q is zeroed
proof end;

theorem Th19: :: LATTICE5:19
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L st d is symmetric holds
for q being Element of [:A,A,the carrier of L,the carrier of L:] holds new_bi_fun d,q is symmetric
proof end;

theorem Th20: :: LATTICE5:20
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L st d is symmetric & d is u.t.i. holds
for q being Element of [:A,A,the carrier of L,the carrier of L:] st d . (q `1 ),(q `2 ) <= (q `3 ) "\/" (q `4 ) holds
new_bi_fun d,q is u.t.i.
proof end;

theorem :: LATTICE5:21
canceled;

theorem Th22: :: LATTICE5:22
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for q being Element of [:A,A,the carrier of L,the carrier of L:] holds d c= new_bi_fun d,q
proof end;

definition
let A be non empty set ;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
func DistEsti d -> Cardinal means :Def12: :: LATTICE5:def 12
it,{ [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . x,y <= a "\/" b } are_equipotent ;
existence
ex b1 being Cardinal st b1,{ [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . x,y <= a "\/" b } are_equipotent
proof end;
uniqueness
for b1, b2 being Cardinal st b1,{ [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . x,y <= a "\/" b } are_equipotent & b2,{ [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . x,y <= a "\/" b } are_equipotent holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines DistEsti LATTICE5:def 12 :
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for b4 being Cardinal holds
( b4 = DistEsti d iff b4,{ [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . x,y <= a "\/" b } are_equipotent );

theorem Th23: :: LATTICE5:23
for A being non empty set
for L being lower-bounded LATTICE
for d being distance_function of A,L holds DistEsti d <> {}
proof end;

definition
let A be non empty set ;
let O be Ordinal;
func ConsecutiveSet A,O -> set means :Def13: :: LATTICE5:def 13
 ex L0 being T-Sequence st
( it = last L0 & dom L0 = succ O & L0 . {} = A & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = new_set (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds
L0 . C = union (rng (L0 | C)) ) );
correctness
existence
ex b1 being set ex L0 being T-Sequence st
( b1 = last L0 & dom L0 = succ O & L0 . {} = A & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = new_set (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds
L0 . C = union (rng (L0 | C)) ) );
uniqueness
for b1, b2 being set st ex L0 being T-Sequence st
( b1 = last L0 & dom L0 = succ O & L0 . {} = A & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = new_set (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds
L0 . C = union (rng (L0 | C)) ) ) & ex L0 being T-Sequence st
( b2 = last L0 & dom L0 = succ O & L0 . {} = A & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = new_set (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds
L0 . C = union (rng (L0 | C)) ) ) holds
b1 = b2;
proof end;
end;

:: deftheorem Def13 defines ConsecutiveSet LATTICE5:def 13 :
for A being non empty set
for O being Ordinal
for b3 being set holds
( b3 = ConsecutiveSet A,O iff ex L0 being T-Sequence st
( b3 = last L0 & dom L0 = succ O & L0 . {} = A & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = new_set (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds
L0 . C = union (rng (L0 | C)) ) ) );

theorem Th24: :: LATTICE5:24
for A being non empty set holds ConsecutiveSet A,{} = A
proof end;

theorem Th25: :: LATTICE5:25
for A being non empty set
for O being Ordinal holds ConsecutiveSet A,(succ O) = new_set (ConsecutiveSet A,O)
proof end;

theorem Th26: :: LATTICE5:26
for A being non empty set
for T being T-Sequence
for O being Ordinal st O <> {} & O is limit_ordinal & dom T = O & ( for O1 being Ordinal st O1 in O holds
T . O1 = ConsecutiveSet A,O1 ) holds
ConsecutiveSet A,O = union (rng T)
proof end;

registration
let A be non empty set ;
let O be Ordinal;
cluster ConsecutiveSet A,O -> non empty ;
coherence
not ConsecutiveSet A,O is empty
proof end;
end;

theorem Th27: :: LATTICE5:27
for A being non empty set
for O being Ordinal holds A c= ConsecutiveSet A,O
proof end;

definition
let A be non empty set ;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
mode QuadrSeq of d -> T-Sequence of [:A,A,the carrier of L,the carrier of L:] means :Def14: :: LATTICE5:def 14
( dom it is Cardinal & it is one-to-one & rng it = { [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . x,y <= a "\/" b } );
existence
ex b1 being T-Sequence of [:A,A,the carrier of L,the carrier of L:] st
( dom b1 is Cardinal & b1 is one-to-one & rng b1 = { [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . x,y <= a "\/" b } )
proof end;
end;

:: deftheorem Def14 defines QuadrSeq LATTICE5:def 14 :
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for b4 being T-Sequence of [:A,A,the carrier of L,the carrier of L:] holds
( b4 is QuadrSeq of d iff ( dom b4 is Cardinal & b4 is one-to-one & rng b4 = { [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . x,y <= a "\/" b } ) );

definition
let A be non empty set ;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
let q be QuadrSeq of d;
let O be Ordinal;
assume A1: O in dom q ;
func Quadr q,O -> Element of [:(ConsecutiveSet A,O),(ConsecutiveSet A,O),the carrier of L,the carrier of L:] equals :Def15: :: LATTICE5:def 15
q . O;
correctness
coherence
q . O is Element of [:(ConsecutiveSet A,O),(ConsecutiveSet A,O),the carrier of L,the carrier of L:];
proof end;
end;

:: deftheorem Def15 defines Quadr LATTICE5:def 15 :
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for q being QuadrSeq of d
for O being Ordinal st O in dom q holds
Quadr q,O = q . O;

theorem Th28: :: LATTICE5:28
for A being non empty set
for L being lower-bounded LATTICE
for O being Ordinal
for d being BiFunction of A,L
for q being QuadrSeq of d holds
( O in DistEsti d iff O in dom q )
proof end;

definition
let A be non empty set ;
let L be lower-bounded LATTICE;
let z be set ;
assume A1: z is BiFunction of A,L ;
func BiFun z,A,L -> BiFunction of A,L equals :Def16: :: LATTICE5:def 16
z;
coherence
z is BiFunction of A,L by A1;
end;

:: deftheorem Def16 defines BiFun LATTICE5:def 16 :
for A being non empty set
for L being lower-bounded LATTICE
for z being set st z is BiFunction of A,L holds
BiFun z,A,L = z;

definition
let A be non empty set ;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
let q be QuadrSeq of d;
let O be Ordinal;
func ConsecutiveDelta q,O -> set means :Def17: :: LATTICE5:def 17
 ex L0 being T-Sequence st
( it = last L0 & dom L0 = succ O & L0 . {} = d & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = new_bi_fun (BiFun (L0 . C),(ConsecutiveSet A,C),L),(Quadr q,C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds
L0 . C = union (rng (L0 | C)) ) );
correctness
existence
ex b1 being set ex L0 being T-Sequence st
( b1 = last L0 & dom L0 = succ O & L0 . {} = d & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = new_bi_fun (BiFun (L0 . C),(ConsecutiveSet A,C),L),(Quadr q,C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds
L0 . C = union (rng (L0 | C)) ) );
uniqueness
for b1, b2 being set st ex L0 being T-Sequence st
( b1 = last L0 & dom L0 = succ O & L0 . {} = d & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = new_bi_fun (BiFun (L0 . C),(ConsecutiveSet A,C),L),(Quadr q,C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds
L0 . C = union (rng (L0 | C)) ) ) & ex L0 being T-Sequence st
( b2 = last L0 & dom L0 = succ O & L0 . {} = d & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = new_bi_fun (BiFun (L0 . C),(ConsecutiveSet A,C),L),(Quadr q,C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds
L0 . C = union (rng (L0 | C)) ) ) holds
b1 = b2;
proof end;
end;

:: deftheorem Def17 defines ConsecutiveDelta LATTICE5:def 17 :
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for q being QuadrSeq of d
for O being Ordinal
for b6 being set holds
( b6 = ConsecutiveDelta q,O iff ex L0 being T-Sequence st
( b6 = last L0 & dom L0 = succ O & L0 . {} = d & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = new_bi_fun (BiFun (L0 . C),(ConsecutiveSet A,C),L),(Quadr q,C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds
L0 . C = union (rng (L0 | C)) ) ) );

theorem Th29: :: LATTICE5:29
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for q being QuadrSeq of d holds ConsecutiveDelta q,{} = d
proof end;

theorem Th30: :: LATTICE5:30
for A being non empty set
for L being lower-bounded LATTICE
for O being Ordinal
for d being BiFunction of A,L
for q being QuadrSeq of d holds ConsecutiveDelta q,(succ O) = new_bi_fun (BiFun (ConsecutiveDelta q,O),(ConsecutiveSet A,O),L),(Quadr q,O)
proof end;

theorem Th31: :: LATTICE5:31
for A being non empty set
for L being lower-bounded LATTICE
for T being T-Sequence
for O being Ordinal
for d being BiFunction of A,L
for q being QuadrSeq of d st O <> {} & O is limit_ordinal & dom T = O & ( for O1 being Ordinal st O1 in O holds
T . O1 = ConsecutiveDelta q,O1 ) holds
ConsecutiveDelta q,O = union (rng T)
proof end;

theorem Th32: :: LATTICE5:32
for A being non empty set
for O1, O2 being Ordinal st O1 c= O2 holds
ConsecutiveSet A,O1 c= ConsecutiveSet A,O2
proof end;

theorem Th33: :: LATTICE5:33
for A being non empty set
for L being lower-bounded LATTICE
for O being Ordinal
for d being BiFunction of A,L
for q being QuadrSeq of d holds ConsecutiveDelta q,O is BiFunction of (ConsecutiveSet A,O),L
proof end;

definition
let A be non empty set ;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
let q be QuadrSeq of d;
let O be Ordinal;
:: original: ConsecutiveDelta
redefine func ConsecutiveDelta q,O -> BiFunction of (ConsecutiveSet A,O),L;
coherence
ConsecutiveDelta q,O is BiFunction of (ConsecutiveSet A,O),L by Th33;
end;

theorem Th34: :: LATTICE5:34
for A being non empty set
for L being lower-bounded LATTICE
for O being Ordinal
for d being BiFunction of A,L
for q being QuadrSeq of d holds d c= ConsecutiveDelta q,O
proof end;

theorem Th35: :: LATTICE5:35
for A being non empty set
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
proof end;

theorem Th36: :: LATTICE5:36
for A being non empty set
for L being lower-bounded LATTICE
for O being Ordinal
for d being BiFunction of A,L st d is zeroed holds
for q being QuadrSeq of d holds ConsecutiveDelta q,O is zeroed
proof end;

theorem Th37: :: LATTICE5:37
for A being non empty set
for L being lower-bounded LATTICE
for O being Ordinal
for d being BiFunction of A,L st d is symmetric holds
for q being QuadrSeq of d holds ConsecutiveDelta q,O is symmetric
proof end;

theorem Th38: :: LATTICE5:38
for A being non empty set
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.
proof end;

theorem :: LATTICE5:39
for A being non empty set
for L being lower-bounded LATTICE
for O being Ordinal
for d being distance_function of A,L
for q being QuadrSeq of d st O c= DistEsti d holds
ConsecutiveDelta q,O is distance_function of (ConsecutiveSet A,O),L by Th36, Th37, Th38;

definition
let A be non empty set ;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
func NextSet d -> set equals :: LATTICE5:def 18
 ConsecutiveSet A,(DistEsti d);
correctness
coherence
ConsecutiveSet A,(DistEsti d) is set ;
;
end;

:: deftheorem defines NextSet LATTICE5:def 18 :
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L holds NextSet d = ConsecutiveSet A,(DistEsti d);

registration
let A be non empty set ;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
cluster NextSet d -> non empty ;
coherence
not NextSet d is empty ;
end;

definition
let A be non empty set ;
let L be lower-bounded LATTICE;
let d be BiFunction of A,L;
let q be QuadrSeq of d;
func NextDelta q -> set equals :: LATTICE5:def 19
 ConsecutiveDelta q,(DistEsti d);
correctness
coherence
ConsecutiveDelta q,(DistEsti d) is set ;
;
end;

:: deftheorem defines NextDelta LATTICE5:def 19 :
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for q being QuadrSeq of d holds NextDelta q = ConsecutiveDelta q,(DistEsti d);

definition
let A be non empty set ;
let L be lower-bounded LATTICE;
let d be distance_function of A,L;
let q be QuadrSeq of d;
:: original: NextDelta
redefine func NextDelta q -> distance_function of (NextSet d),L;
coherence
NextDelta q is distance_function of (NextSet d),L by Th36, Th37, Th38;
end;

definition
let A be non empty set ;
let L be lower-bounded LATTICE;
let d be distance_function of A,L;
let Aq be non empty set ;
let dq be distance_function of Aq,L;
pred Aq,dq is_extension_of A,d means :Def20: :: LATTICE5:def 20
 ex q being QuadrSeq of d st
( Aq = NextSet d & dq = NextDelta q );
end;

:: deftheorem Def20 defines is_extension_of LATTICE5:def 20 :
for A being non empty set
for L being lower-bounded LATTICE
for d being distance_function of A,L
for Aq being non empty set
for dq being distance_function of Aq,L holds
( Aq,dq is_extension_of A,d iff ex q being QuadrSeq of d st
( Aq = NextSet d & dq = NextDelta q ) );

theorem Th40: :: LATTICE5:40
for A being non empty set
for L being lower-bounded LATTICE
for d being distance_function of A,L
for Aq being non empty set
for dq being distance_function of Aq,L st Aq,dq is_extension_of A,d holds
for x, y being Element of A
for a, b being Element of L st d . x,y <= a "\/" b holds
ex z1, z2, z3 being Element of Aq st
( dq . x,z1 = a & dq . z2,z3 = a & dq . z1,z2 = b & dq . z3,y = b )
proof end;

definition
let A be non empty set ;
let L be lower-bounded LATTICE;
let d be distance_function of A,L;
mode ExtensionSeq of A,d -> Function means :Def21: :: LATTICE5:def 21
( dom it = NAT & it . 0 = [A,d] & ( for n being Element of NAT ex A' being non empty set ex d' being distance_function of A',L ex Aq being non empty set ex dq being distance_function of Aq,L st
( Aq,dq is_extension_of A',d' & it . n = [A',d'] & it . (n + 1) = [Aq,dq] ) ) );
existence
ex b1 being Function st
( dom b1 = NAT & b1 . 0 = [A,d] & ( for n being Element of NAT ex A' being non empty set ex d' being distance_function of A',L ex Aq being non empty set ex dq being distance_function of Aq,L st
( Aq,dq is_extension_of A',d' & b1 . n = [A',d'] & b1 . (n + 1) = [Aq,dq] ) ) )
proof end;
end;

:: deftheorem Def21 defines ExtensionSeq LATTICE5:def 21 :
for A being non empty set
for L being lower-bounded LATTICE
for d being distance_function of A,L
for b4 being Function holds
( b4 is ExtensionSeq of A,d iff ( dom b4 = NAT & b4 . 0 = [A,d] & ( for n being Element of NAT ex A' being non empty set ex d' being distance_function of A',L ex Aq being non empty set ex dq being distance_function of Aq,L st
( Aq,dq is_extension_of A',d' & b4 . n = [A',d'] & b4 . (n + 1) = [Aq,dq] ) ) ) );

theorem Th41: :: LATTICE5:41
for A being non empty set
for L being lower-bounded LATTICE
for d being distance_function of A,L
for S being ExtensionSeq of A,d
for k, l being Element of NAT st k <= l holds
(S . k) `1 c= (S . l) `1
proof end;

theorem Th42: :: LATTICE5:42
for A being non empty set
for L being lower-bounded LATTICE
for d being distance_function of A,L
for S being ExtensionSeq of A,d
for k, l being Element of NAT st k <= l holds
(S . k) `2 c= (S . l) `2
proof end;

definition
let L be lower-bounded LATTICE;
func BasicDF L -> distance_function of the carrier of L,L means :Def22: :: LATTICE5:def 22
for x, y being Element of L holds
( ( x <> y implies it . x,y = x "\/" y ) & ( x = y implies it . x,y = Bottom L ) );
existence
ex b1 being distance_function of the carrier of L,L st
for x, y being Element of L holds
( ( x <> y implies b1 . x,y = x "\/" y ) & ( x = y implies b1 . x,y = Bottom L ) )
proof end;
uniqueness
for b1, b2 being distance_function of the carrier of L,L st ( for x, y being Element of L holds
( ( x <> y implies b1 . x,y = x "\/" y ) & ( x = y implies b1 . x,y = Bottom L ) ) ) & ( for x, y being Element of L holds
( ( x <> y implies b2 . x,y = x "\/" y ) & ( x = y implies b2 . x,y = Bottom L ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def22 defines BasicDF LATTICE5:def 22 :
for L being lower-bounded LATTICE
for b2 being distance_function of the carrier of L,L holds
( b2 = BasicDF L iff for x, y being Element of L holds
( ( x <> y implies b2 . x,y = x "\/" y ) & ( x = y implies b2 . x,y = Bottom L ) ) );

theorem Th43: :: LATTICE5:43
for L being lower-bounded LATTICE holds BasicDF L is onto
proof end;

Lm2: now
let j be Element of NAT ; :: thesis: ( 1 <= j & j < 5 & not j = 1 & not j = 2 & not j = 3 implies j = 4 )
assume A1: ( 1 <= j & j < 5 ) ; :: thesis: ( j = 1 or j = 2 or j = 3 or j = 4 )
then j < 4 + 1 ;
then j <= 4 by NAT_1:13;
then ( j = 0 or j = 1 or j = 2 or j = 3 or j = 4 ) by NAT_1:29;
hence ( j = 1 or j = 2 or j = 3 or j = 4 ) by A1; :: thesis: verum
end;

Lm3: now
let m be Element of NAT ; :: thesis: ( not m in Seg 5 or m = 1 or m = 2 or m = 3 or m = 4 or m = 5 )
assume A1: m in Seg 5 ; :: thesis: ( m = 1 or m = 2 or m = 3 or m = 4 or m = 5 )
then ( 1 <= m & m <= 5 ) by FINSEQ_1:3;
then ( m = 0 or m = 1 or m = 2 or m = 3 or m = 4 or m = 5 ) by NAT_1:30;
hence ( m = 1 or m = 2 or m = 3 or m = 4 or m = 5 ) by A1, FINSEQ_1:3; :: thesis: verum
end;

Lm4: now
let A be non empty set ; :: thesis: for L being lower-bounded LATTICE
for d being distance_function of A,L holds succ {} c= DistEsti d
let L be lower-bounded LATTICE; :: thesis: for d being distance_function of A,L holds succ {} c= DistEsti d
let d be distance_function of A,L; :: thesis: succ {} c= DistEsti d
( succ {} c= DistEsti d or DistEsti d in succ {} ) by ORDINAL1:26;
then ( succ {} c= DistEsti d or DistEsti d c= {} ) by ORDINAL1:34;
hence succ {} c= DistEsti d by Th23, XBOOLE_1:3; :: thesis: verum
end;

theorem Th44: :: LATTICE5:44
for L being lower-bounded LATTICE
for S being ExtensionSeq of the carrier of L, BasicDF L
for FS being non empty set st FS = union { ((S . i) `1 ) where i is Element of NAT : verum } holds
union { ((S . i) `2 ) where i is Element of NAT : verum } is distance_function of FS,L
proof end;

theorem Th45: :: LATTICE5:45
for L being lower-bounded LATTICE
for S being ExtensionSeq of the carrier of L, BasicDF L
for FS being non empty set
for FD being distance_function of FS,L
for x, y being Element of FS
for a, b being Element of L st FS = union { ((S . i) `1 ) where i is Element of NAT : verum } & FD = union { ((S . i) `2 ) where i is Element of NAT : verum } & FD . x,y <= a "\/" b holds
ex z1, z2, z3 being Element of FS st
( FD . x,z1 = a & FD . z2,z3 = a & FD . z1,z2 = b & FD . z3,y = b )
proof end;

theorem Th46: :: LATTICE5:46
for L being lower-bounded LATTICE
for S being ExtensionSeq of the carrier of L, BasicDF L
for FS being non empty set
for FD being distance_function of FS,L
for f being Homomorphism of L,(EqRelLATT FS)
for x, y being Element of FS
for e1, e2 being Equivalence_Relation of FS
for x, y being set st f = alpha FD & FS = union { ((S . i) `1 ) where i is Element of NAT : verum } & FD = union { ((S . i) `2 ) where i is Element of NAT : verum } & e1 in the carrier of (Image f) & e2 in the carrier of (Image f) & [x,y] in e1 "\/" e2 holds
ex F being non empty FinSequence of FS st
( len F = 3 + 2 & x,y are_joint_by F,e1,e2 )
proof end;

theorem :: LATTICE5:47
for L being lower-bounded LATTICE ex A being non empty set ex f being Homomorphism of L,(EqRelLATT A) st
( f is one-to-one & type_of (Image f) <= 3 )
proof end;