:: LATTICE5 semantic presentation

scheme :: LATTICE5:sch 1
RecChoice{ F₁() -> set , P₁[ set , set , set ] } :

ex f being Function st
( dom f = NAT & f . 0 = F₁() & ( for n being Element of NAT holds P₁[n,f . n,f . (n + 1)] ) )

provided

A1: for n being Nat
for x being set ex y being set st P₁[n,x,y]

proof end;

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 ;

end;

:: deftheorem defines EqRelLATT LATTICE5:def 1 :

registration

let A be set ;
cluster EqRelLATT A -> with_suprema with_infima ;
coherence ;

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

proof end;

end;

:: deftheorem defines complete LATTICE5:def 2 :

registration

let A be set ;
cluster EqRelLATT A -> with_suprema with_infima complete ;
coherence

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

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

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

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 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 :

theorem :: LATTICE5:11

canceled;

theorem Th12: :: LATTICE5:12

for X being non empty set
for x being set
for o being 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 Nat; :: thesis:
assume ( 1 <= i & i < n + m ) ; :: thesis:
then ( ( 1 <= i & i < n ) or ( n = i & i < n + m ) or ( n < i & i < n + m ) ) by REAL_1:def 5;
hence ( ( 1 <= i & i < n ) or ( n = i & i < n + m ) or ( n + 1 <= i & i < n + m ) ) by NAT_1:38; :: thesis:

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 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 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 -> 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines type_of LATTICE5:def 4 :

theorem Th15: :: LATTICE5:15

for X being non empty set
for Y being Sublattice of EqRelLATT X
for n being 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 non empty set ;
let L be lower-bounded LATTICE;
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 lower-bounded LATTICE;
let f be BiFunction of A,L;
let x, y be Element of A;
:: original: .
redefine func f . x,y -> Element of L;
coherence

proof end;

end;

definition

let A be non empty set ;
let L be lower-bounded LATTICE;
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;
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 LATTICE5:def 5 :

:: deftheorem Def6 defines symmetric LATTICE5:def 6 :

:: deftheorem Def7 defines zeroed LATTICE5:def 7 :

:: deftheorem Def8 defines u.t.i. LATTICE5:def 8 :

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

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines alpha LATTICE5:def 9 :

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 ;

end;

:: deftheorem defines new_set LATTICE5:def 10 :

registration

let A be set ;
cluster new_set A -> non empty ;
coherence

proof end;

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines new_bi_fun LATTICE5:def 11 :

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 Th21: :: LATTICE5:21

for A being set holds A c= new_set A by XBOOLE_1:7;

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines DistEsti LATTICE5:def 12 :

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

proof end;

end;

:: deftheorem Def13 defines ConsecutiveSet LATTICE5:def 13 :

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

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

proof end;

end;

:: deftheorem Def14 defines QuadrSeq LATTICE5:def 14 :

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

proof end;

end;

:: deftheorem Def15 defines Quadr LATTICE5:def 15 :

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 by A1;

end;

:: deftheorem Def16 defines BiFun LATTICE5:def 16 :

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

proof end;

end;

:: deftheorem Def17 defines ConsecutiveDelta LATTICE5:def 17 :

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 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 ;

end;

:: deftheorem defines NextSet LATTICE5:def 18 :

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 ;

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 ;

end;

:: deftheorem defines NextDelta LATTICE5:def 19 :

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 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 :

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 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

proof end;

end;

:: deftheorem Def21 defines ExtensionSeq LATTICE5:def 21 :

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 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 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def22 defines BasicDF LATTICE5:def 22 :

theorem Th43: :: LATTICE5:43

for L being lower-bounded LATTICE holds BasicDF L is onto

proof end;

Lm2: now

let j be Nat; :: thesis:
assume A1: ( 1 <= j & j < 5 ) ; :: thesis:
then j < 4 + 1 ;
then j <= 4 by NAT_1:38;
then ( j = 0 or j = 1 or j = 2 or j = 3 or j = 4 ) by CQC_THE1:5;
hence ( j = 1 or j = 2 or j = 3 or j = 4 ) by A1; :: thesis:

end;

Lm3: now

let m be Nat; :: thesis:
assume A1: m in Seg 5 ; :: thesis:
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 CQC_THE1:6;
hence ( m = 1 or m = 2 or m = 3 or m = 4 or m = 5 ) by A1, FINSEQ_1:3; :: thesis:

end;

Lm4: now

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

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 Nat : verum } holds
union { ((S . i) `2 ) where i is 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 Nat : verum } & FD = union { ((S . i) `2 ) where i is 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 Nat : verum } & FD = union { ((S . i) `2 ) where i is 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;