:: J\'onsson Theorem
:: by Jaros{\l}aw Gryko
::
:: Received November 13, 1997
:: Copyright (c) 1997-2021 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 Relation-like the carrier of L1 -defined the carrier of L2 -valued Function-like quasi_total meet-preserving join-preserving for Element of bool [: 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 for 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;

registration
let L1, L2 be LATTICE;
let f be Homomorphism of L1,L2;
cluster Image f -> meet-inheriting join-inheriting ;
coherence
( Image f is meet-inheriting & Image f is join-inheriting )
proof end;
end;

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

:: deftheorem 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 object
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
( ( i is odd implies [(f . i),(f . (i + 1))] in R1 ) & ( i is even implies [(f . i),(f . (i + 1))] in R2 ) ) ) ) );

theorem Th11: :: LATTICE5:11
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 :: thesis: for i, n, m being Element of NAT st 1 <= i & i < n + m & not ( 1 <= i & i < n ) & not ( n = i & i < n + m ) holds
( n + 1 <= i & i < n + m )
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 Th12: :: LATTICE5:12
for X being non empty set
for x, y being object
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 object 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 object 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 object 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 object 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 object 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 object 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 object 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 object 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 object 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 object 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 object 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 object 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 Th13: :: LATTICE5:13
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 object 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;
attr f is symmetric means :Def5: :: LATTICE5:def 5
 for x, y being Element of A holds f . (x,y) = f . (y,x);
end;

:: deftheorem Def5 defines symmetric LATTICE5:def 5 :
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 :Def6: :: LATTICE5:def 6
 for x being Element of A holds f . (x,x) = Bottom L;
attr f is u.t.i. means :Def7: :: LATTICE5:def 7
 for x, y, z being Element of A holds (f . (x,y)) "\/" (f . (y,z)) >= f . (x,z);
end;

:: deftheorem Def6 defines zeroed LATTICE5:def 6 :
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 Def7 defines u.t.i. 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 u.t.i. iff for x, y, z being Element of A holds (f . (x,y)) "\/" (f . (y,z)) >= f . (x,z) );

:: f is u.t.i. means that f satisfies the triangle inequality
registration
let A be non empty set ;
let L be lower-bounded LATTICE;
cluster Relation-like [:A,A:] -defined the carrier of L -valued Function-like quasi_total symmetric zeroed u.t.i. for Element of bool [:[: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 :Def8: :: LATTICE5:def 8
 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 Def8 defines alpha LATTICE5:def 8 :
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 Th14: :: LATTICE5:14
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 Th15: :: LATTICE5:15
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 9
A \/ {{A},{{A}},{{{A}}}};
correctness
coherence
A \/ {{A},{{A}},{{{A}}}} is set ;
;
end;

:: deftheorem defines new_set LATTICE5:def 9 :
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 :Def10: :: LATTICE5:def 10
( ( 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_4 & it . ({{{A}}},{{A}}) = q `3_4 & it . ({A},{{A}}) = q `4_4 & it . ({{A}},{A}) = q `4_4 & it . ({A},{{{A}}}) = (q `3_4) "\/" (q `4_4) & it . ({{{A}}},{A}) = (q `3_4) "\/" (q `4_4) & ( for u being Element of A holds
( it . (u,{A}) = (d . (u,(q `1_4))) "\/" (q `3_4) & it . ({A},u) = (d . (u,(q `1_4))) "\/" (q `3_4) & it . (u,{{A}}) = ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & it . ({{A}},u) = ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & it . (u,{{{A}}}) = (d . (u,(q `2_4))) "\/" (q `4_4) & it . ({{{A}}},u) = (d . (u,(q `2_4))) "\/" (q `4_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_4 & b1 . ({{{A}}},{{A}}) = q `3_4 & b1 . ({A},{{A}}) = q `4_4 & b1 . ({{A}},{A}) = q `4_4 & b1 . ({A},{{{A}}}) = (q `3_4) "\/" (q `4_4) & b1 . ({{{A}}},{A}) = (q `3_4) "\/" (q `4_4) & ( for u being Element of A holds
( b1 . (u,{A}) = (d . (u,(q `1_4))) "\/" (q `3_4) & b1 . ({A},u) = (d . (u,(q `1_4))) "\/" (q `3_4) & b1 . (u,{{A}}) = ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & b1 . ({{A}},u) = ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & b1 . (u,{{{A}}}) = (d . (u,(q `2_4))) "\/" (q `4_4) & b1 . ({{{A}}},u) = (d . (u,(q `2_4))) "\/" (q `4_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_4 & b1 . ({{{A}}},{{A}}) = q `3_4 & b1 . ({A},{{A}}) = q `4_4 & b1 . ({{A}},{A}) = q `4_4 & b1 . ({A},{{{A}}}) = (q `3_4) "\/" (q `4_4) & b1 . ({{{A}}},{A}) = (q `3_4) "\/" (q `4_4) & ( for u being Element of A holds
( b1 . (u,{A}) = (d . (u,(q `1_4))) "\/" (q `3_4) & b1 . ({A},u) = (d . (u,(q `1_4))) "\/" (q `3_4) & b1 . (u,{{A}}) = ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & b1 . ({{A}},u) = ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & b1 . (u,{{{A}}}) = (d . (u,(q `2_4))) "\/" (q `4_4) & b1 . ({{{A}}},u) = (d . (u,(q `2_4))) "\/" (q `4_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_4 & b2 . ({{{A}}},{{A}}) = q `3_4 & b2 . ({A},{{A}}) = q `4_4 & b2 . ({{A}},{A}) = q `4_4 & b2 . ({A},{{{A}}}) = (q `3_4) "\/" (q `4_4) & b2 . ({{{A}}},{A}) = (q `3_4) "\/" (q `4_4) & ( for u being Element of A holds
( b2 . (u,{A}) = (d . (u,(q `1_4))) "\/" (q `3_4) & b2 . ({A},u) = (d . (u,(q `1_4))) "\/" (q `3_4) & b2 . (u,{{A}}) = ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & b2 . ({{A}},u) = ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & b2 . (u,{{{A}}}) = (d . (u,(q `2_4))) "\/" (q `4_4) & b2 . ({{{A}}},u) = (d . (u,(q `2_4))) "\/" (q `4_4) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines new_bi_fun LATTICE5:def 10 :
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_4 & b5 . ({{{A}}},{{A}}) = q `3_4 & b5 . ({A},{{A}}) = q `4_4 & b5 . ({{A}},{A}) = q `4_4 & b5 . ({A},{{{A}}}) = (q `3_4) "\/" (q `4_4) & b5 . ({{{A}}},{A}) = (q `3_4) "\/" (q `4_4) & ( for u being Element of A holds
( b5 . (u,{A}) = (d . (u,(q `1_4))) "\/" (q `3_4) & b5 . ({A},u) = (d . (u,(q `1_4))) "\/" (q `3_4) & b5 . (u,{{A}}) = ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & b5 . ({{A}},u) = ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & b5 . (u,{{{A}}}) = (d . (u,(q `2_4))) "\/" (q `4_4) & b5 . ({{{A}}},u) = (d . (u,(q `2_4))) "\/" (q `4_4) ) ) ) );

theorem Th16: :: LATTICE5:16
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 Th17: :: LATTICE5:17
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 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 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_4),(q `2_4)) <= (q `3_4) "\/" (q `4_4) holds
new_bi_fun (d,q) is u.t.i.
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
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 :Def11: :: LATTICE5:def 11
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 by WELLORD2:15, CARD_1:2;
end;

:: deftheorem Def11 defines DistEsti LATTICE5:def 11 :
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 Th20: :: LATTICE5:20
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 :Def12: :: LATTICE5:def 12
 ex L0 being Sequence st
( it = last L0 & dom L0 = succ O & L0 . 0 = 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 <> 0 & C is limit_ordinal holds
L0 . C = union (rng (L0 | C)) ) );
correctness
existence
ex b1 being set ex L0 being Sequence st
( b1 = last L0 & dom L0 = succ O & L0 . 0 = 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 <> 0 & C is limit_ordinal holds
L0 . C = union (rng (L0 | C)) ) );
uniqueness
for b1, b2 being set st ex L0 being Sequence st
( b1 = last L0 & dom L0 = succ O & L0 . 0 = 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 <> 0 & C is limit_ordinal holds
L0 . C = union (rng (L0 | C)) ) ) & ex L0 being Sequence st
( b2 = last L0 & dom L0 = succ O & L0 . 0 = 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 <> 0 & C is limit_ordinal holds
L0 . C = union (rng (L0 | C)) ) ) holds
b1 = b2;
proof end;
end;

:: deftheorem Def12 defines ConsecutiveSet LATTICE5:def 12 :
for A being non empty set
for O being Ordinal
for b3 being set holds
( b3 = ConsecutiveSet (A,O) iff ex L0 being Sequence st
( b3 = last L0 & dom L0 = succ O & L0 . 0 = 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 <> 0 & C is limit_ordinal holds
L0 . C = union (rng (L0 | C)) ) ) );

theorem Th21: :: LATTICE5:21
for A being non empty set holds ConsecutiveSet (A,0) = A
proof end;

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

theorem Th23: :: LATTICE5:23
for A being non empty set
for T being Sequence
for O being Ordinal st O <> 0 & 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 Th24: :: LATTICE5:24
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 -> Sequence of [:A,A, the carrier of L, the carrier of L:] means :Def13: :: LATTICE5:def 13
( 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 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 Def13 defines QuadrSeq LATTICE5:def 13 :
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for b4 being 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 :Def14: :: LATTICE5:def 14
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 Def14 defines Quadr LATTICE5:def 14 :
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 Th25: :: LATTICE5:25
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 :Def15: :: LATTICE5:def 15
z;
coherence
z is BiFunction of A,L by A1;
end;

:: deftheorem Def15 defines BiFun LATTICE5:def 15 :
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 :Def16: :: LATTICE5:def 16
 ex L0 being Sequence st
( it = last L0 & dom L0 = succ O & L0 . 0 = 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 <> 0 & C is limit_ordinal holds
L0 . C = union (rng (L0 | C)) ) );
correctness
existence
ex b1 being set ex L0 being Sequence st
( b1 = last L0 & dom L0 = succ O & L0 . 0 = 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 <> 0 & C is limit_ordinal holds
L0 . C = union (rng (L0 | C)) ) );
uniqueness
for b1, b2 being set st ex L0 being Sequence st
( b1 = last L0 & dom L0 = succ O & L0 . 0 = 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 <> 0 & C is limit_ordinal holds
L0 . C = union (rng (L0 | C)) ) ) & ex L0 being Sequence st
( b2 = last L0 & dom L0 = succ O & L0 . 0 = 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 <> 0 & C is limit_ordinal holds
L0 . C = union (rng (L0 | C)) ) ) holds
b1 = b2;
proof end;
end;

:: deftheorem Def16 defines ConsecutiveDelta LATTICE5:def 16 :
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 Sequence st
( b6 = last L0 & dom L0 = succ O & L0 . 0 = 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 <> 0 & C is limit_ordinal holds
L0 . C = union (rng (L0 | C)) ) ) );

theorem Th26: :: LATTICE5:26
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,0) = d
proof end;

theorem Th27: :: LATTICE5:27
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 Th28: :: LATTICE5:28
for A being non empty set
for L being lower-bounded LATTICE
for T being Sequence
for O being Ordinal
for d being BiFunction of A,L
for q being QuadrSeq of d st O <> 0 & 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 Th29: :: LATTICE5:29
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 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,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 Th30;
end;

theorem Th31: :: LATTICE5:31
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 Th32: :: LATTICE5:32
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 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 st d is zeroed holds
for q being QuadrSeq of d holds ConsecutiveDelta (q,O) is zeroed
proof 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 st d is symmetric holds
for q being QuadrSeq of d holds ConsecutiveDelta (q,O) is symmetric
proof end;

theorem Th35: :: LATTICE5:35
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:36
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 Th33, Th34, Th35;

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 17
 ConsecutiveSet (A,(DistEsti d));
correctness
coherence
ConsecutiveSet (A,(DistEsti d)) is set ;
;
end;

:: deftheorem defines NextSet LATTICE5:def 17 :
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 18
 ConsecutiveDelta (q,(DistEsti d));
correctness
coherence
ConsecutiveDelta (q,(DistEsti d)) is set ;
;
end;

:: deftheorem defines NextDelta LATTICE5:def 18 :
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 Th33, Th34, Th35;
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 :: LATTICE5:def 19
 ex q being QuadrSeq of d st
( Aq = NextSet d & dq = NextDelta q );
end;

:: deftheorem defines is_extension_of LATTICE5:def 19 :
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 Th37: :: LATTICE5:37
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 :Def20: :: LATTICE5:def 20
( dom it = NAT & it . 0 = [A,d] & ( for n being Nat ex A9 being non empty set ex d9 being distance_function of A9,L ex Aq being non empty set ex dq being distance_function of Aq,L st
( Aq,dq is_extension_of A9,d9 & it . n = [A9,d9] & it . (n + 1) = [Aq,dq] ) ) );
existence
ex b1 being Function st
( dom b1 = NAT & b1 . 0 = [A,d] & ( for n being Nat ex A9 being non empty set ex d9 being distance_function of A9,L ex Aq being non empty set ex dq being distance_function of Aq,L st
( Aq,dq is_extension_of A9,d9 & b1 . n = [A9,d9] & b1 . (n + 1) = [Aq,dq] ) ) )
proof end;
end;

:: deftheorem Def20 defines ExtensionSeq LATTICE5:def 20 :
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 Nat ex A9 being non empty set ex d9 being distance_function of A9,L ex Aq being non empty set ex dq being distance_function of Aq,L st
( Aq,dq is_extension_of A9,d9 & b4 . n = [A9,d9] & b4 . (n + 1) = [Aq,dq] ) ) ) );

theorem Th38: :: LATTICE5:38
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 Nat st k <= l holds
(S . k) `1 c= (S . l) `1
proof end;

theorem Th39: :: LATTICE5:39
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 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 :Def21: :: LATTICE5:def 21
 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 Def21 defines BasicDF LATTICE5:def 21 :
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 Th40: :: LATTICE5:40
for L being lower-bounded LATTICE holds BasicDF L is onto
proof end;

Lm2: now :: thesis: for j being Nat st 1 <= j & j < 5 holds
not not j = 1 & ... & not j = 4
let j be Nat; :: thesis: ( 1 <= j & j < 5 implies not not j = 1 & ... & not j = 4 )
assume that
A1: 1 <= j and
A2: j < 5 ; :: thesis: not not j = 1 & ... & not j = 4
j < 4 + 1 by A2;
then j <= 4 by NAT_1:13;
then not not j = 0 & ... & not j = 4 by NAT_1:60;
hence not not j = 1 & ... & not j = 4 by A1; :: thesis: verum
end;

Lm3: now :: thesis: for m being Element of NAT st m in Seg 5 holds
not not m = 1 & ... & not m = 5
let m be Element of NAT ; :: thesis: ( m in Seg 5 implies not not m = 1 & ... & not m = 5 )
assume A1: m in Seg 5 ; :: thesis: not not m = 1 & ... & not m = 5
then m <= 5 by FINSEQ_1:1;
then not not m = 0 & ... & not m = 5 by NAT_1:60;
hence not not m = 1 & ... & not m = 5 by A1, FINSEQ_1:1; :: thesis: verum
end;

Lm4: now :: thesis: for A being non empty set
for L being lower-bounded LATTICE
for d being distance_function of A,L holds succ {} c= DistEsti d
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:16;
then ( succ {} c= DistEsti d or DistEsti d c= {} ) by ORDINAL1:22;
hence succ {} c= DistEsti d by Th20, XBOOLE_1:3; :: thesis: verum
end;

theorem Th41: :: LATTICE5:41
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 Th42: :: LATTICE5:42
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 Th43: :: LATTICE5:43
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 object 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;

:: WP: Jonsson Theorem for lattices
theorem :: LATTICE5:44
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;