:: LATTICE2 semantic presentation

begin


theorem Th1: :: LATTICE2:1
for A being set
for C being non empty set
for B being Subset of A
for g being Function of A,C holds dom (g | B) = B
proof
let A be set ; ::_thesis: for C being non empty set
for B being Subset of A
for g being Function of A,C holds dom (g | B) = B
let C be non empty set ; ::_thesis: for B being Subset of A
for g being Function of A,C holds dom (g | B) = B
let B be Subset of A; ::_thesis: for g being Function of A,C holds dom (g | B) = B
let g be Function of A,C; ::_thesis: dom (g | B) = B
thus  dom (g | B) = (dom g) /\ B by RELAT_1:61
.= A /\ B by FUNCT_2:def_1
.= B by XBOOLE_1:28 ; ::_thesis: verum
end;

theorem Th2: :: LATTICE2:2
for A being set
for C being non empty set
for B being Subset of A
for f, g being Function of A,C holds
( f | B = g | B iff for x being Element of A st x in B holds
g . x = f . x )
proof
let A be set ; ::_thesis: for C being non empty set
for B being Subset of A
for f, g being Function of A,C holds
( f | B = g | B iff for x being Element of A st x in B holds
g . x = f . x )
let C be non empty set ; ::_thesis: for B being Subset of A
for f, g being Function of A,C holds
( f | B = g | B iff for x being Element of A st x in B holds
g . x = f . x )
let B be Subset of A; ::_thesis: for f, g being Function of A,C holds
( f | B = g | B iff for x being Element of A st x in B holds
g . x = f . x )
let f, g be Function of A,C; ::_thesis: ( f | B = g | B iff for x being Element of A st x in B holds
g . x = f . x )
thus  ( f | B = g | B implies for x being Element of A st x in B holds
g . x = f . x ) ::_thesis: ( ( for x being Element of A st x in B holds
g . x = f . x ) implies f | B = g | B )
proof
assume A1: f | B = g | B ; ::_thesis: for x being Element of A st x in B holds
g . x = f . x
let x be Element of A; ::_thesis: ( x in B implies g . x = f . x )
assume A2: x in B ; ::_thesis: g . x = f . x
hence g . x = (g | B) . x by FUNCT_1:49
.= f . x by A1, A2, FUNCT_1:49 ;
::_thesis: verum
end;
reconsider f9 = f | B, g9 = g | B as Function of B,C by FUNCT_2:32;
assume A3: for x being Element of A st x in B holds
g . x = f . x ; ::_thesis: f | B = g | B
A4: now__::_thesis:_for_x_being_set_st_x_in_B_holds_
f9_._x_=_g9_._x
let x be set ; ::_thesis: ( x in B implies f9 . x = g9 . x )
assume A5: x in B ; ::_thesis: f9 . x = g9 . x
hence f9 . x = f . x by FUNCT_1:49
.= g . x by A3, A5
.= g9 . x by A5, FUNCT_1:49 ;
::_thesis: verum
end;
thus f | B = f9 | B
.= g9 | B by A4, FUNCT_2:12
.= g | B ; ::_thesis: verum
end;

theorem Th3: :: LATTICE2:3
for A being set
for C being non empty set
for f, g being Function of A,C
for B being set holds f +* (g | B) is Function of A,C
proof
let A be set ; ::_thesis: for C being non empty set
for f, g being Function of A,C
for B being set holds f +* (g | B) is Function of A,C
let C be non empty set ; ::_thesis: for f, g being Function of A,C
for B being set holds f +* (g | B) is Function of A,C
let f, g be Function of A,C; ::_thesis: for B being set holds f +* (g | B) is Function of A,C
let B be set ; ::_thesis: f +* (g | B) is Function of A,C
A1: ( dom f = A & dom g = A ) by FUNCT_2:def_1;
dom (f +* (g | B)) = (dom f) \/ (dom (g | B)) by FUNCT_4:def_1
.= (dom f) \/ ((dom g) /\ B) by RELAT_1:61
.= A by A1, XBOOLE_1:22 ;
hence  f +* (g | B) is Function of A,C by FUNCT_2:67; ::_thesis: verum
end;

theorem Th4: :: LATTICE2:4
for A being set
for C being non empty set
for B being Subset of A
for g, f being Function of A,C holds (g | B) +* f = f
proof
let A be set ; ::_thesis: for C being non empty set
for B being Subset of A
for g, f being Function of A,C holds (g | B) +* f = f
let C be non empty set ; ::_thesis: for B being Subset of A
for g, f being Function of A,C holds (g | B) +* f = f
let B be Subset of A; ::_thesis: for g, f being Function of A,C holds (g | B) +* f = f
let g, f be Function of A,C; ::_thesis: (g | B) +* f = f
 ( dom (g | B) = B & dom f = A ) by Th1, FUNCT_2:def_1;
hence  (g | B) +* f = f by FUNCT_4:19; ::_thesis: verum
end;

theorem Th5: :: LATTICE2:5
for f, g being Function st g c= f holds
f +* g = f
proof
let f, g be Function; ::_thesis: ( g c= f implies f +* g = f )
assume A1: g c= f ; ::_thesis: f +* g = f
then  dom g c= dom f by GRFUNC_1:2;
then A2: dom f = (dom f) \/ (dom g) by XBOOLE_1:12;
 for x being set st x in dom f holds
( ( x in dom g implies f . x = g . x ) & ( not x in dom g implies f . x = f . x ) ) by A1, GRFUNC_1:2;
hence  f +* g = f by A2, FUNCT_4:def_1; ::_thesis: verum
end;

theorem :: LATTICE2:6
for A being set
for C being non empty set
for B being Subset of A
for f being Function of A,C holds f +* (f | B) = f by Th5, RELAT_1:59;

theorem Th7: :: LATTICE2:7
for A being set
for C being non empty set
for B being Subset of A
for g, f being Function of A,C st ( for x being Element of A st x in B holds
g . x = f . x ) holds
f +* (g | B) = f
proof
let A be set ; ::_thesis: for C being non empty set
for B being Subset of A
for g, f being Function of A,C st ( for x being Element of A st x in B holds
g . x = f . x ) holds
f +* (g | B) = f
let C be non empty set ; ::_thesis: for B being Subset of A
for g, f being Function of A,C st ( for x being Element of A st x in B holds
g . x = f . x ) holds
f +* (g | B) = f
let B be Subset of A; ::_thesis: for g, f being Function of A,C st ( for x being Element of A st x in B holds
g . x = f . x ) holds
f +* (g | B) = f
let g, f be Function of A,C; ::_thesis: ( ( for x being Element of A st x in B holds
g . x = f . x ) implies f +* (g | B) = f )
assume  for x being Element of A st x in B holds
g . x = f . x ; ::_thesis: f +* (g | B) = f
then  g | B = f | B by Th2;
hence  f +* (g | B) = f by Th5, RELAT_1:59; ::_thesis: verum
end;

theorem :: LATTICE2:8
for A being set
for C being non empty set
for g, f being Function of A,C
for B being Finite_Subset of A holds (g | B) +* f = f
proof
let A be set ; ::_thesis: for C being non empty set
for g, f being Function of A,C
for B being Finite_Subset of A holds (g | B) +* f = f
let C be non empty set ; ::_thesis: for g, f being Function of A,C
for B being Finite_Subset of A holds (g | B) +* f = f
let g, f be Function of A,C; ::_thesis: for B being Finite_Subset of A holds (g | B) +* f = f
let B be Finite_Subset of A; ::_thesis: (g | B) +* f = f
reconsider C = B as Subset of A by FINSUB_1:17;
 (g | C) +* f = f by Th4;
hence  (g | B) +* f = f ; ::_thesis: verum
end;

theorem Th9: :: LATTICE2:9
for A being set
for C being non empty set
for g being Function of A,C
for B being Finite_Subset of A holds dom (g | B) = B
proof
let A be set ; ::_thesis: for C being non empty set
for g being Function of A,C
for B being Finite_Subset of A holds dom (g | B) = B
let C be non empty set ; ::_thesis: for g being Function of A,C
for B being Finite_Subset of A holds dom (g | B) = B
let g be Function of A,C; ::_thesis: for B being Finite_Subset of A holds dom (g | B) = B
let B be Finite_Subset of A; ::_thesis: dom (g | B) = B
reconsider C = B as Subset of A by FINSUB_1:17;
 dom (g | C) = C by Th1;
hence  dom (g | B) = B ; ::_thesis: verum
end;

theorem Th10: :: LATTICE2:10
for A being set
for C being non empty set
for g, f being Function of A,C
for B being Finite_Subset of A st ( for x being Element of A st x in B holds
g . x = f . x ) holds
f +* (g | B) = f
proof
let A be set ; ::_thesis: for C being non empty set
for g, f being Function of A,C
for B being Finite_Subset of A st ( for x being Element of A st x in B holds
g . x = f . x ) holds
f +* (g | B) = f
let C be non empty set ; ::_thesis: for g, f being Function of A,C
for B being Finite_Subset of A st ( for x being Element of A st x in B holds
g . x = f . x ) holds
f +* (g | B) = f
let g, f be Function of A,C; ::_thesis: for B being Finite_Subset of A st ( for x being Element of A st x in B holds
g . x = f . x ) holds
f +* (g | B) = f
let B be Finite_Subset of A; ::_thesis: ( ( for x being Element of A st x in B holds
g . x = f . x ) implies f +* (g | B) = f )
reconsider C = B as Subset of A by FINSUB_1:17;
 ( ( for x being Element of A st x in C holds
g . x = f . x ) implies f +* (g | C) = f ) by Th7;
hence  ( ( for x being Element of A st x in B holds
g . x = f . x ) implies f +* (g | B) = f ) ; ::_thesis: verum
end;

definition
let D be non empty set ;
let o, o9 be BinOp of D;
predo absorbs o9 means :Def1: :: LATTICE2:def 1
 for x, y being Element of D holds o . (x,(o9 . (x,y))) = x;
end;

:: deftheorem Def1 defines absorbs LATTICE2:def_1_:_
 for D being non empty set
for o, o9 being BinOp of D holds
( o absorbs o9 iff for x, y being Element of D holds o . (x,(o9 . (x,y))) = x );

notation
let D be non empty set ;
let o, o9 be BinOp of D;
antonym o doesn't_absorb o9 for o absorbs o9;
end;


theorem Th11: :: LATTICE2:11
for L being non empty LattStr st the L_join of L is commutative & the L_join of L is associative & the L_meet of L is commutative & the L_meet of L is associative & the L_join of L absorbs the L_meet of L & the L_meet of L absorbs the L_join of L holds
L is Lattice-like
proof
let L be non empty LattStr ; ::_thesis: ( the L_join of L is commutative & the L_join of L is associative & the L_meet of L is commutative & the L_meet of L is associative & the L_join of L absorbs the L_meet of L & the L_meet of L absorbs the L_join of L implies L is Lattice-like )
assume that
A1: the L_join of L is commutative and
A2: the L_join of L is associative and
A3: the L_meet of L is commutative and
A4: the L_meet of L is associative and
A5: the L_join of L absorbs the L_meet of L and
A6: the L_meet of L absorbs the L_join of L ; ::_thesis: L is Lattice-like
thus  for a, b being Element of L holds a "\/" b = b "\/" a by A1, BINOP_1:def_2; :: according to LATTICES:def_4,LATTICES:def_10 ::_thesis: ( L is join-associative & L is meet-absorbing & L is meet-commutative & L is meet-associative & L is join-absorbing )
thus  for a, b, c being Element of L holds a "\/" (b "\/" c) = (a "\/" b) "\/" c by A2, BINOP_1:def_3; :: according to LATTICES:def_5 ::_thesis: ( L is meet-absorbing & L is meet-commutative & L is meet-associative & L is join-absorbing )
thus  for a, b being Element of L holds (a "/\" b) "\/" b = b :: according to LATTICES:def_8 ::_thesis: ( L is meet-commutative & L is meet-associative & L is join-absorbing )
proof
let a, b be Element of L; ::_thesis: (a "/\" b) "\/" b = b
thus (a "/\" b) "\/" b = b "\/" (a "/\" b) by A1, BINOP_1:def_2
.= b "\/" (b "/\" a) by A3, BINOP_1:def_2
.= b by A5, Def1 ; ::_thesis: verum
end;
thus  for a, b being Element of L holds a "/\" b = b "/\" a by A3, BINOP_1:def_2; :: according to LATTICES:def_6 ::_thesis: ( L is meet-associative & L is join-absorbing )
thus  for a, b, c being Element of L holds a "/\" (b "/\" c) = (a "/\" b) "/\" c by A4, BINOP_1:def_3; :: according to LATTICES:def_7 ::_thesis: L is join-absorbing
let a be Element of L; :: according to LATTICES:def_9 ::_thesis: for b1 being Element of the carrier of L holds a "/\" (a "\/" b1) = a
let b be Element of L; ::_thesis: a "/\" (a "\/" b) = a
thus  a "/\" (a "\/" b) = a by A6, Def1; ::_thesis: verum
end;

definition
let L be LattStr ;
funcL .:  ->  strict LattStr  equals :: LATTICE2:def 2
 LattStr(# the carrier of L, the L_meet of L, the L_join of L #);
correctness
coherence
LattStr(# the carrier of L, the L_meet of L, the L_join of L #) is strict LattStr ;
;
end;

:: deftheorem  defines .: LATTICE2:def_2_:_
 for L being LattStr holds L .: = LattStr(# the carrier of L, the L_meet of L, the L_join of L #);

registration
let L be non empty LattStr ;
clusterL .:  ->  non empty strict ;
coherence
 not L .: is empty ;
end;

theorem :: LATTICE2:12
for L being non empty LattStr holds
( the carrier of L = the carrier of (L .:) & the L_join of L = the L_meet of (L .:) & the L_meet of L = the L_join of (L .:) ) ;

theorem :: LATTICE2:13
for L being non empty strict LattStr holds (L .:) .: = L ;


theorem Th14: :: LATTICE2:14
for L being Lattice
for u being Element of L st ( for v being Element of L holds u "\/" v = v ) holds
u = Bottom L
proof
let L be Lattice; ::_thesis: for u being Element of L st ( for v being Element of L holds u "\/" v = v ) holds
u = Bottom L
let u be Element of L; ::_thesis: ( ( for v being Element of L holds u "\/" v = v ) implies u = Bottom L )
assume A1: for v being Element of L holds u "\/" v = v ; ::_thesis: u = Bottom L
now__::_thesis:_for_v_being_Element_of_L_holds_v_"/\"_u_=_u
let v be Element of L; ::_thesis: v "/\" u = u
 v "\/" u = v by A1;
then  u [= v by LATTICES:def_3;
hence  v "/\" u = u by LATTICES:4; ::_thesis: verum
end;
hence  u = Bottom L by RLSUB_2:64; ::_thesis: verum
end;

theorem Th15: :: LATTICE2:15
for L being Lattice
for u being Element of L st ( for v being Element of L holds the L_join of L . (u,v) = v ) holds
u = Bottom L
proof
let L be Lattice; ::_thesis: for u being Element of L st ( for v being Element of L holds the L_join of L . (u,v) = v ) holds
u = Bottom L
let u be Element of L; ::_thesis: ( ( for v being Element of L holds the L_join of L . (u,v) = v ) implies u = Bottom L )
assume  for v being Element of L holds the L_join of L . (u,v) = v ; ::_thesis: u = Bottom L
then  for v being Element of L holds u "\/" v = v ;
hence  u = Bottom L by Th14; ::_thesis: verum
end;

theorem Th16: :: LATTICE2:16
for L being Lattice
for u being Element of L st ( for v being Element of L holds u "/\" v = v ) holds
u = Top L
proof
let L be Lattice; ::_thesis: for u being Element of L st ( for v being Element of L holds u "/\" v = v ) holds
u = Top L
let u be Element of L; ::_thesis: ( ( for v being Element of L holds u "/\" v = v ) implies u = Top L )
assume A1: for v being Element of L holds u "/\" v = v ; ::_thesis: u = Top L
now__::_thesis:_for_v_being_Element_of_L_holds_u_=_v_"\/"_u
let v be Element of L; ::_thesis: u = v "\/" u
 v "/\" u = v by A1;
then  v [= u by LATTICES:4;
hence  u = v "\/" u by LATTICES:def_3; ::_thesis: verum
end;
hence  u = Top L by RLSUB_2:65; ::_thesis: verum
end;

theorem Th17: :: LATTICE2:17
for L being Lattice
for u being Element of L st ( for v being Element of L holds the L_meet of L . (u,v) = v ) holds
u = Top L
proof
let L be Lattice; ::_thesis: for u being Element of L st ( for v being Element of L holds the L_meet of L . (u,v) = v ) holds
u = Top L
let u be Element of L; ::_thesis: ( ( for v being Element of L holds the L_meet of L . (u,v) = v ) implies u = Top L )
assume  for v being Element of L holds the L_meet of L . (u,v) = v ; ::_thesis: u = Top L
then  for v being Element of L holds u "/\" v = v ;
hence  u = Top L by Th16; ::_thesis: verum
end;

registration
let L be Lattice;
cluster the L_join of L ->  idempotent ;
coherence
 the L_join of L is idempotent
proof
let a be Element of L; :: according to BINOP_1:def_4 ::_thesis: the L_join of L . (a,a) = a
thus  the L_join of L . (a,a) = a "\/" a
.= a ; ::_thesis: verum
end;
end;

registration
let L be non empty join-commutative \/-SemiLattStr ;
cluster the L_join of L ->  commutative ;
coherence
 the L_join of L is commutative
proof
let a, b be Element of L; :: according to BINOP_1:def_2 ::_thesis: the L_join of L . (a,b) = the L_join of L . (b,a)
thus  the L_join of L . (a,b) = b "\/" a by LATTICES:def_1
.= the L_join of L . (b,a) ; ::_thesis: verum
end;
end;

theorem Th18: :: LATTICE2:18
for L being Lattice st the L_join of L is having_a_unity holds
Bottom L = the_unity_wrt the L_join of L
proof
let L be Lattice; ::_thesis: ( the L_join of L is having_a_unity implies Bottom L = the_unity_wrt the L_join of L )
set J = the L_join of L;
given u being Element of L such that A1: u is_a_unity_wrt the L_join of L ; :: according to SETWISEO:def_2 ::_thesis: Bottom L = the_unity_wrt the L_join of L
 for v being Element of L holds the L_join of L . (u,v) = v by A1, BINOP_1:4;
then  u = Bottom L by Th15;
hence  Bottom L = the_unity_wrt the L_join of L by A1, BINOP_1:def_8; ::_thesis: verum
end;

registration
let L be non empty join-associative \/-SemiLattStr ;
cluster the L_join of L ->  associative ;
coherence
 the L_join of L is associative
proof
let a, b, c be Element of L; :: according to BINOP_1:def_3 ::_thesis: the L_join of L . (a,( the L_join of L . (b,c))) = the L_join of L . (( the L_join of L . (a,b)),c)
thus  the L_join of L . (a,( the L_join of L . (b,c))) = a "\/" (b "\/" c)
.= (a "\/" b) "\/" c by LATTICES:def_5
.= the L_join of L . (( the L_join of L . (a,b)),c) ; ::_thesis: verum
end;
end;

registration
let L be Lattice;
cluster the L_meet of L ->  idempotent ;
coherence
 the L_meet of L is idempotent
proof
let a be Element of L; :: according to BINOP_1:def_4 ::_thesis: the L_meet of L . (a,a) = a
thus  the L_meet of L . (a,a) = a "/\" a
.= a ; ::_thesis: verum
end;
end;

registration
let L be non empty meet-commutative /\-SemiLattStr ;
cluster the L_meet of L ->  commutative ;
coherence
 the L_meet of L is commutative
proof
let a, b be Element of L; :: according to BINOP_1:def_2 ::_thesis: the L_meet of L . (a,b) = the L_meet of L . (b,a)
thus  the L_meet of L . (a,b) = b "/\" a by LATTICES:def_2
.= the L_meet of L . (b,a) ; ::_thesis: verum
end;
end;

registration
let L be non empty meet-associative /\-SemiLattStr ;
cluster the L_meet of L ->  associative ;
coherence
 the L_meet of L is associative
proof
let a, b, c be Element of L; :: according to BINOP_1:def_3 ::_thesis: the L_meet of L . (a,( the L_meet of L . (b,c))) = the L_meet of L . (( the L_meet of L . (a,b)),c)
thus  the L_meet of L . (a,( the L_meet of L . (b,c))) = a "/\" (b "/\" c)
.= (a "/\" b) "/\" c by LATTICES:def_7
.= the L_meet of L . (( the L_meet of L . (a,b)),c) ; ::_thesis: verum
end;
end;

theorem Th19: :: LATTICE2:19
for L being Lattice st the L_meet of L is having_a_unity holds
Top L = the_unity_wrt the L_meet of L
proof
let L be Lattice; ::_thesis: ( the L_meet of L is having_a_unity implies Top L = the_unity_wrt the L_meet of L )
set J = the L_meet of L;
given u being Element of L such that A1: u is_a_unity_wrt the L_meet of L ; :: according to SETWISEO:def_2 ::_thesis: Top L = the_unity_wrt the L_meet of L
 for v being Element of L holds the L_meet of L . (u,v) = v by A1, BINOP_1:4;
then  u = Top L by Th17;
hence  Top L = the_unity_wrt the L_meet of L by A1, BINOP_1:def_8; ::_thesis: verum
end;

theorem Th20: :: LATTICE2:20
for L being Lattice holds the L_join of L is_distributive_wrt the L_join of L
proof
let L be Lattice; ::_thesis: the L_join of L is_distributive_wrt the L_join of L
now__::_thesis:_for_a,_b,_c_being_Element_of_L_holds_the_L_join_of_L_._(a,(_the_L_join_of_L_._(b,c)))_=_the_L_join_of_L_._((_the_L_join_of_L_._(a,b)),(_the_L_join_of_L_._(a,c)))
let a, b, c be Element of L; ::_thesis: the L_join of L . (a,( the L_join of L . (b,c))) = the L_join of L . (( the L_join of L . (a,b)),( the L_join of L . (a,c)))
thus  the L_join of L . (a,( the L_join of L . (b,c))) = a "\/" (b "\/" c)
.= (a "\/" b) "\/" c by LATTICES:def_5
.= ((a "\/" a) "\/" b) "\/" c
.= ((a "\/" b) "\/" a) "\/" c by LATTICES:def_5
.= (a "\/" b) "\/" (a "\/" c) by LATTICES:def_5
.= the L_join of L . (( the L_join of L . (a,b)),( the L_join of L . (a,c))) ; ::_thesis: verum
end;
hence  the L_join of L is_distributive_wrt the L_join of L by BINOP_1:12; ::_thesis: verum
end;

theorem :: LATTICE2:21
for L being Lattice st L is D_Lattice holds
the L_join of L is_distributive_wrt the L_meet of L
proof
let L be Lattice; ::_thesis: ( L is D_Lattice implies the L_join of L is_distributive_wrt the L_meet of L )
assume A1: L is D_Lattice ; ::_thesis: the L_join of L is_distributive_wrt the L_meet of L
now__::_thesis:_for_a,_b,_c_being_Element_of_L_holds_the_L_join_of_L_._(a,(_the_L_meet_of_L_._(b,c)))_=_the_L_meet_of_L_._((_the_L_join_of_L_._(a,b)),(_the_L_join_of_L_._(a,c)))
let a, b, c be Element of L; ::_thesis: the L_join of L . (a,( the L_meet of L . (b,c))) = the L_meet of L . (( the L_join of L . (a,b)),( the L_join of L . (a,c)))
thus  the L_join of L . (a,( the L_meet of L . (b,c))) = a "\/" (b "/\" c)
.= (a "\/" b) "/\" (a "\/" c) by A1, LATTICES:11
.= the L_meet of L . (( the L_join of L . (a,b)),( the L_join of L . (a,c))) ; ::_thesis: verum
end;
hence  the L_join of L is_distributive_wrt the L_meet of L by BINOP_1:12; ::_thesis: verum
end;

theorem Th22: :: LATTICE2:22
for L being Lattice st the L_join of L is_distributive_wrt the L_meet of L holds
L is distributive
proof
let L be Lattice; ::_thesis: ( the L_join of L is_distributive_wrt the L_meet of L implies L is distributive )
assume A1: the L_join of L is_distributive_wrt the L_meet of L ; ::_thesis: L is distributive
then A2: for a, b, c being Element of L holds a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c) by BINOP_1:12;
let a be Element of L; :: according to LATTICES:def_11 ::_thesis: for b1, b2 being Element of the carrier of L holds a "/\" (b1 "\/" b2) = (a "/\" b1) "\/" (a "/\" b2)
let b, c be Element of L; ::_thesis: a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c)
thus a "/\" (b "\/" c) = (a "/\" (c "\/" a)) "/\" (c "\/" b) by LATTICES:def_9
.= a "/\" ((c "\/" a) "/\" (c "\/" b)) by LATTICES:def_7
.= a "/\" ((a "/\" b) "\/" c) by A2
.= ((a "/\" b) "\/" a) "/\" ((a "/\" b) "\/" c) by LATTICES:def_8
.= (a "/\" b) "\/" (a "/\" c) by A1, BINOP_1:12 ; ::_thesis: verum
end;

theorem Th23: :: LATTICE2:23
for L being Lattice st L is D_Lattice holds
the L_meet of L is_distributive_wrt the L_join of L
proof
let L be Lattice; ::_thesis: ( L is D_Lattice implies the L_meet of L is_distributive_wrt the L_join of L )
assume A1: L is D_Lattice ; ::_thesis: the L_meet of L is_distributive_wrt the L_join of L
now__::_thesis:_for_a,_b,_c_being_Element_of_L_holds_the_L_meet_of_L_._(a,(_the_L_join_of_L_._(b,c)))_=_the_L_join_of_L_._((_the_L_meet_of_L_._(a,b)),(_the_L_meet_of_L_._(a,c)))
let a, b, c be Element of L; ::_thesis: the L_meet of L . (a,( the L_join of L . (b,c))) = the L_join of L . (( the L_meet of L . (a,b)),( the L_meet of L . (a,c)))
thus  the L_meet of L . (a,( the L_join of L . (b,c))) = a "/\" (b "\/" c)
.= (a "/\" b) "\/" (a "/\" c) by A1, LATTICES:def_11
.= the L_join of L . (( the L_meet of L . (a,b)),( the L_meet of L . (a,c))) ; ::_thesis: verum
end;
hence  the L_meet of L is_distributive_wrt the L_join of L by BINOP_1:12; ::_thesis: verum
end;

theorem :: LATTICE2:24
for L being Lattice st the L_meet of L is_distributive_wrt the L_join of L holds
L is distributive
proof
let L be Lattice; ::_thesis: ( the L_meet of L is_distributive_wrt the L_join of L implies L is distributive )
assume A1: the L_meet of L is_distributive_wrt the L_join of L ; ::_thesis: L is distributive
let a be Element of L; :: according to LATTICES:def_11 ::_thesis: for b1, b2 being Element of the carrier of L holds a "/\" (b1 "\/" b2) = (a "/\" b1) "\/" (a "/\" b2)
let b, c be Element of L; ::_thesis: a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c)
thus  a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c) by A1, BINOP_1:12; ::_thesis: verum
end;

theorem Th25: :: LATTICE2:25
for L being Lattice holds the L_meet of L is_distributive_wrt the L_meet of L
proof
let L be Lattice; ::_thesis: the L_meet of L is_distributive_wrt the L_meet of L
now__::_thesis:_for_a,_b,_c_being_Element_of_L_holds_the_L_meet_of_L_._(a,(_the_L_meet_of_L_._(b,c)))_=_the_L_meet_of_L_._((_the_L_meet_of_L_._(a,b)),(_the_L_meet_of_L_._(a,c)))
let a, b, c be Element of L; ::_thesis: the L_meet of L . (a,( the L_meet of L . (b,c))) = the L_meet of L . (( the L_meet of L . (a,b)),( the L_meet of L . (a,c)))
thus  the L_meet of L . (a,( the L_meet of L . (b,c))) = a "/\" (b "/\" c)
.= (a "/\" b) "/\" c by LATTICES:def_7
.= ((a "/\" a) "/\" b) "/\" c
.= ((a "/\" b) "/\" a) "/\" c by LATTICES:def_7
.= (a "/\" b) "/\" (a "/\" c) by LATTICES:def_7
.= the L_meet of L . (( the L_meet of L . (a,b)),( the L_meet of L . (a,c))) ; ::_thesis: verum
end;
hence  the L_meet of L is_distributive_wrt the L_meet of L by BINOP_1:12; ::_thesis: verum
end;

theorem Th26: :: LATTICE2:26
for L being Lattice holds the L_join of L absorbs the L_meet of L
proof
let L be Lattice; ::_thesis: the L_join of L absorbs the L_meet of L
let x, y be Element of L; :: according to LATTICE2:def_1 ::_thesis: the L_join of L . (x,( the L_meet of L . (x,y))) = x
thus  the L_join of L . (x,( the L_meet of L . (x,y))) = x "\/" (x "/\" y)
.= x by LATTICES:def_8 ; ::_thesis: verum
end;

theorem Th27: :: LATTICE2:27
for L being Lattice holds the L_meet of L absorbs the L_join of L
proof
let L be Lattice; ::_thesis: the L_meet of L absorbs the L_join of L
let x, y be Element of L; :: according to LATTICE2:def_1 ::_thesis: the L_meet of L . (x,( the L_join of L . (x,y))) = x
thus  the L_meet of L . (x,( the L_join of L . (x,y))) = x "/\" (x "\/" y)
.= x by LATTICES:def_9 ; ::_thesis: verum
end;

definition
let A be non empty set ;
let L be Lattice;
let B be Finite_Subset of A;
let f be Function of A, the carrier of L;
func FinJoin (B,f) ->  Element of L equals :: LATTICE2:def 3
 the L_join of L $$ (B,f);
correctness
coherence
the L_join of L $$ (B,f) is Element of L;
;
func FinMeet (B,f) ->  Element of L equals :: LATTICE2:def 4
 the L_meet of L $$ (B,f);
correctness
coherence
the L_meet of L $$ (B,f) is Element of L;
;
end;

:: deftheorem  defines FinJoin LATTICE2:def_3_:_
 for A being non empty set
for L being Lattice
for B being Finite_Subset of A
for f being Function of A, the carrier of L holds FinJoin (B,f) = the L_join of L $$ (B,f);

:: deftheorem  defines FinMeet LATTICE2:def_4_:_
 for A being non empty set
for L being Lattice
for B being Finite_Subset of A
for f being Function of A, the carrier of L holds FinMeet (B,f) = the L_meet of L $$ (B,f);


theorem Th28: :: LATTICE2:28
for L being Lattice
for A being non empty set
for x being Element of A
for B being Finite_Subset of A
for f being Function of A, the carrier of L st x in B holds
f . x [= FinJoin (B,f)
proof
let L be Lattice; ::_thesis: for A being non empty set
for x being Element of A
for B being Finite_Subset of A
for f being Function of A, the carrier of L st x in B holds
f . x [= FinJoin (B,f)
let A be non empty set ; ::_thesis: for x being Element of A
for B being Finite_Subset of A
for f being Function of A, the carrier of L st x in B holds
f . x [= FinJoin (B,f)
let x be Element of A; ::_thesis: for B being Finite_Subset of A
for f being Function of A, the carrier of L st x in B holds
f . x [= FinJoin (B,f)
let B be Finite_Subset of A; ::_thesis: for f being Function of A, the carrier of L st x in B holds
f . x [= FinJoin (B,f)
let f be Function of A, the carrier of L; ::_thesis: ( x in B implies f . x [= FinJoin (B,f) )
assume  x in B ; ::_thesis: f . x [= FinJoin (B,f)
then  (f . x) "\/" (FinJoin (B,f)) = FinJoin (B,f) by SETWISEO:22;
hence  f . x [= FinJoin (B,f) by LATTICES:def_3; ::_thesis: verum
end;

theorem Th29: :: LATTICE2:29
for L being Lattice
for u being Element of L
for A being non empty set
for B being Finite_Subset of A
for f being Function of A, the carrier of L st ex x being Element of A st
( x in B & u [= f . x ) holds
u [= FinJoin (B,f)
proof
let L be Lattice; ::_thesis: for u being Element of L
for A being non empty set
for B being Finite_Subset of A
for f being Function of A, the carrier of L st ex x being Element of A st
( x in B & u [= f . x ) holds
u [= FinJoin (B,f)
let u be Element of L; ::_thesis: for A being non empty set
for B being Finite_Subset of A
for f being Function of A, the carrier of L st ex x being Element of A st
( x in B & u [= f . x ) holds
u [= FinJoin (B,f)
let A be non empty set ; ::_thesis: for B being Finite_Subset of A
for f being Function of A, the carrier of L st ex x being Element of A st
( x in B & u [= f . x ) holds
u [= FinJoin (B,f)
let B be Finite_Subset of A; ::_thesis: for f being Function of A, the carrier of L st ex x being Element of A st
( x in B & u [= f . x ) holds
u [= FinJoin (B,f)
let f be Function of A, the carrier of L; ::_thesis: ( ex x being Element of A st
( x in B & u [= f . x ) implies u [= FinJoin (B,f) )
given x being Element of A such that A1: x in B and
A2: u [= f . x ; ::_thesis: u [= FinJoin (B,f)
 f . x [= FinJoin (B,f) by A1, Th28;
then A3: (f . x) "\/" (FinJoin (B,f)) = FinJoin (B,f) by LATTICES:def_3;
then u "\/" (FinJoin (B,f)) = (u "\/" (f . x)) "\/" (FinJoin (B,f)) by LATTICES:def_5
.= FinJoin (B,f) by A2, A3, LATTICES:def_3 ;
hence  u [= FinJoin (B,f) by LATTICES:def_3; ::_thesis: verum
end;

theorem :: LATTICE2:30
for L being Lattice
for u being Element of L
for A being non empty set
for B being Finite_Subset of A
for f being Function of A, the carrier of L st ( for x being Element of A st x in B holds
f . x = u ) & B <> {} holds
FinJoin (B,f) = u by SETWISEO:24;

theorem :: LATTICE2:31
for L being Lattice
for u being Element of L
for A being non empty set
for B being Finite_Subset of A
for f being Function of A, the carrier of L st FinJoin (B,f) [= u holds
for x being Element of A st x in B holds
f . x [= u
proof
let L be Lattice; ::_thesis: for u being Element of L
for A being non empty set
for B being Finite_Subset of A
for f being Function of A, the carrier of L st FinJoin (B,f) [= u holds
for x being Element of A st x in B holds
f . x [= u
let u be Element of L; ::_thesis: for A being non empty set
for B being Finite_Subset of A
for f being Function of A, the carrier of L st FinJoin (B,f) [= u holds
for x being Element of A st x in B holds
f . x [= u
let A be non empty set ; ::_thesis: for B being Finite_Subset of A
for f being Function of A, the carrier of L st FinJoin (B,f) [= u holds
for x being Element of A st x in B holds
f . x [= u
let B be Finite_Subset of A; ::_thesis: for f being Function of A, the carrier of L st FinJoin (B,f) [= u holds
for x being Element of A st x in B holds
f . x [= u
let f be Function of A, the carrier of L; ::_thesis: ( FinJoin (B,f) [= u implies for x being Element of A st x in B holds
f . x [= u )
assume A1: FinJoin (B,f) [= u ; ::_thesis: for x being Element of A st x in B holds
f . x [= u
let x be Element of A; ::_thesis: ( x in B implies f . x [= u )
assume  x in B ; ::_thesis: f . x [= u
then  f . x [= FinJoin (B,f) by Th28;
hence  f . x [= u by A1, LATTICES:7; ::_thesis: verum
end;

theorem Th32: :: LATTICE2:32
for L being Lattice
for u being Element of L
for A being non empty set
for B being Finite_Subset of A
for f being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds
f . x [= u ) holds
FinJoin (B,f) [= u
proof
let L be Lattice; ::_thesis: for u being Element of L
for A being non empty set
for B being Finite_Subset of A
for f being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds
f . x [= u ) holds
FinJoin (B,f) [= u
let u be Element of L; ::_thesis: for A being non empty set
for B being Finite_Subset of A
for f being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds
f . x [= u ) holds
FinJoin (B,f) [= u
let A be non empty set ; ::_thesis: for B being Finite_Subset of A
for f being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds
f . x [= u ) holds
FinJoin (B,f) [= u
let B be Finite_Subset of A; ::_thesis: for f being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds
f . x [= u ) holds
FinJoin (B,f) [= u
let f be Function of A, the carrier of L; ::_thesis: ( B <> {} & ( for x being Element of A st x in B holds
f . x [= u ) implies FinJoin (B,f) [= u )
assume that
A1: B <> {} and
A2: for x being Element of A st x in B holds
f . x [= u ; ::_thesis: FinJoin (B,f) [= u
set J = the L_join of L;
A3: now__::_thesis:_for_x_being_Element_of_A_st_x_in_B_holds_
(_the_L_join_of_L_[:]_(f,u))_._x_=_u
let x be Element of A; ::_thesis: ( x in B implies ( the L_join of L [:] (f,u)) . x = u )
assume  x in B ; ::_thesis: ( the L_join of L [:] (f,u)) . x = u
then A4: f . x [= u by A2;
thus ( the L_join of L [:] (f,u)) . x = (f . x) "\/" u by FUNCOP_1:48
.= u by A4, LATTICES:def_3 ; ::_thesis: verum
end;
(FinJoin (B,f)) "\/" u = the L_join of L $$ (B,( the L_join of L [:] (f,u))) by A1, Th20, SETWISEO:28
.= u by A1, A3, SETWISEO:24 ;
hence  FinJoin (B,f) [= u by LATTICES:def_3; ::_thesis: verum
end;

theorem :: LATTICE2:33
for L being Lattice
for A being non empty set
for B being Finite_Subset of A
for f, g being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds
f . x [= g . x ) holds
FinJoin (B,f) [= FinJoin (B,g)
proof
let L be Lattice; ::_thesis: for A being non empty set
for B being Finite_Subset of A
for f, g being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds
f . x [= g . x ) holds
FinJoin (B,f) [= FinJoin (B,g)
let A be non empty set ; ::_thesis: for B being Finite_Subset of A
for f, g being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds
f . x [= g . x ) holds
FinJoin (B,f) [= FinJoin (B,g)
let B be Finite_Subset of A; ::_thesis: for f, g being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds
f . x [= g . x ) holds
FinJoin (B,f) [= FinJoin (B,g)
let f, g be Function of A, the carrier of L; ::_thesis: ( B <> {} & ( for x being Element of A st x in B holds
f . x [= g . x ) implies FinJoin (B,f) [= FinJoin (B,g) )
assume that
A1: B <> {} and
A2: for x being Element of A st x in B holds
f . x [= g . x ; ::_thesis: FinJoin (B,f) [= FinJoin (B,g)
now__::_thesis:_for_x_being_Element_of_A_st_x_in_B_holds_
f_._x_[=_FinJoin_(B,g)
let x be Element of A; ::_thesis: ( x in B implies f . x [= FinJoin (B,g) )
assume A3: x in B ; ::_thesis: f . x [= FinJoin (B,g)
then  f . x [= g . x by A2;
hence  f . x [= FinJoin (B,g) by A3, Th29; ::_thesis: verum
end;
hence  FinJoin (B,f) [= FinJoin (B,g) by A1, Th32; ::_thesis: verum
end;

theorem Th34: :: LATTICE2:34
for L being Lattice
for A being non empty set
for B being Finite_Subset of A
for f, g being Function of A, the carrier of L st B <> {} & f | B = g | B holds
FinJoin (B,f) = FinJoin (B,g)
proof
let L be Lattice; ::_thesis: for A being non empty set
for B being Finite_Subset of A
for f, g being Function of A, the carrier of L st B <> {} & f | B = g | B holds
FinJoin (B,f) = FinJoin (B,g)
let A be non empty set ; ::_thesis: for B being Finite_Subset of A
for f, g being Function of A, the carrier of L st B <> {} & f | B = g | B holds
FinJoin (B,f) = FinJoin (B,g)
let B be Finite_Subset of A; ::_thesis: for f, g being Function of A, the carrier of L st B <> {} & f | B = g | B holds
FinJoin (B,f) = FinJoin (B,g)
let f, g be Function of A, the carrier of L; ::_thesis: ( B <> {} & f | B = g | B implies FinJoin (B,f) = FinJoin (B,g) )
assume that
A1: B <> {} and
A2: f | B = g | B ; ::_thesis: FinJoin (B,f) = FinJoin (B,g)
 f .: B = g .: B by A2, RELAT_1:166;
hence  FinJoin (B,f) = FinJoin (B,g) by A1, SETWISEO:26; ::_thesis: verum
end;

theorem :: LATTICE2:35
for L being Lattice
for v being Element of L
for A being non empty set
for B being Finite_Subset of A
for f being Function of A, the carrier of L st B <> {} holds
v "\/" (FinJoin (B,f)) = FinJoin (B,( the L_join of L [;] (v,f))) by Th20, SETWISEO:27;

registration
let L be Lattice;
clusterL .:  ->  strict Lattice-like ;
coherence
 L .: is Lattice-like
proof
 ( the L_join of (L .:) absorbs the L_meet of (L .:) & the L_meet of (L .:) absorbs the L_join of (L .:) ) by Th26, Th27;
hence  L .: is Lattice-like by Th11; ::_thesis: verum
end;
end;

theorem :: LATTICE2:36
for A being non empty set
for L being Lattice
for B being Finite_Subset of A
for f being Function of A, the carrier of L
for f9 being Function of A, the carrier of (L .:) st f = f9 holds
( FinJoin (B,f) = FinMeet (B,f9) & FinMeet (B,f) = FinJoin (B,f9) ) ;

theorem Th37: :: LATTICE2:37
for L being Lattice
for a, b being Element of L
for a9, b9 being Element of (L .:) st a = a9 & b = b9 holds
( a "/\" b = a9 "\/" b9 & a "\/" b = a9 "/\" b9 ) ;

theorem Th38: :: LATTICE2:38
for L being Lattice
for a, b being Element of L st a [= b holds
for a9, b9 being Element of (L .:) st a = a9 & b = b9 holds
b9 [= a9
proof
let L be Lattice; ::_thesis: for a, b being Element of L st a [= b holds
for a9, b9 being Element of (L .:) st a = a9 & b = b9 holds
b9 [= a9
let a, b be Element of L; ::_thesis: ( a [= b implies for a9, b9 being Element of (L .:) st a = a9 & b = b9 holds
b9 [= a9 )
assume  a [= b ; ::_thesis: for a9, b9 being Element of (L .:) st a = a9 & b = b9 holds
b9 [= a9
then A1: a "\/" b = b by LATTICES:def_3;
let a9, b9 be Element of (L .:); ::_thesis: ( a = a9 & b = b9 implies b9 [= a9 )
assume  ( a = a9 & b = b9 ) ; ::_thesis: b9 [= a9
then  b9 "/\" a9 = b9 by A1, Th37;
hence  b9 [= a9 by LATTICES:4; ::_thesis: verum
end;

theorem Th39: :: LATTICE2:39
for L being Lattice
for a, b being Element of L
for a9, b9 being Element of (L .:) st a9 [= b9 & a = a9 & b = b9 holds
b [= a
proof
let L be Lattice; ::_thesis: for a, b being Element of L
for a9, b9 being Element of (L .:) st a9 [= b9 & a = a9 & b = b9 holds
b [= a
let a, b be Element of L; ::_thesis: for a9, b9 being Element of (L .:) st a9 [= b9 & a = a9 & b = b9 holds
b [= a
let a9, b9 be Element of (L .:); ::_thesis: ( a9 [= b9 & a = a9 & b = b9 implies b [= a )
assume that
A1: a9 [= b9 and
A2: ( a = a9 & b = b9 ) ; ::_thesis: b [= a
 a9 "\/" b9 = b9 by A1, LATTICES:def_3;
then  b "/\" a = b by A2, Th37;
hence  b [= a by LATTICES:4; ::_thesis: verum
end;

theorem Th40: :: LATTICE2:40
for L being Lattice
for A being non empty set
for x being Element of A
for B being Finite_Subset of A
for f being Function of A, the carrier of L st x in B holds
FinMeet (B,f) [= f . x
proof
let L be Lattice; ::_thesis: for A being non empty set
for x being Element of A
for B being Finite_Subset of A
for f being Function of A, the carrier of L st x in B holds
FinMeet (B,f) [= f . x
let A be non empty set ; ::_thesis: for x being Element of A
for B being Finite_Subset of A
for f being Function of A, the carrier of L st x in B holds
FinMeet (B,f) [= f . x
let x be Element of A; ::_thesis: for B being Finite_Subset of A
for f being Function of A, the carrier of L st x in B holds
FinMeet (B,f) [= f . x
let B be Finite_Subset of A; ::_thesis: for f being Function of A, the carrier of L st x in B holds
FinMeet (B,f) [= f . x
let f be Function of A, the carrier of L; ::_thesis: ( x in B implies FinMeet (B,f) [= f . x )
reconsider f9 = f as Function of A, the carrier of (L .:) ;
assume  x in B ; ::_thesis: FinMeet (B,f) [= f . x
then  f9 . x [= FinJoin (B,f9) by Th28;
hence  FinMeet (B,f) [= f . x by Th39; ::_thesis: verum
end;

theorem Th41: :: LATTICE2:41
for L being Lattice
for u being Element of L
for A being non empty set
for B being Finite_Subset of A
for f being Function of A, the carrier of L st ex x being Element of A st
( x in B & f . x [= u ) holds
FinMeet (B,f) [= u
proof
let L be Lattice; ::_thesis: for u being Element of L
for A being non empty set
for B being Finite_Subset of A
for f being Function of A, the carrier of L st ex x being Element of A st
( x in B & f . x [= u ) holds
FinMeet (B,f) [= u
let u be Element of L; ::_thesis: for A being non empty set
for B being Finite_Subset of A
for f being Function of A, the carrier of L st ex x being Element of A st
( x in B & f . x [= u ) holds
FinMeet (B,f) [= u
let A be non empty set ; ::_thesis: for B being Finite_Subset of A
for f being Function of A, the carrier of L st ex x being Element of A st
( x in B & f . x [= u ) holds
FinMeet (B,f) [= u
let B be Finite_Subset of A; ::_thesis: for f being Function of A, the carrier of L st ex x being Element of A st
( x in B & f . x [= u ) holds
FinMeet (B,f) [= u
let f be Function of A, the carrier of L; ::_thesis: ( ex x being Element of A st
( x in B & f . x [= u ) implies FinMeet (B,f) [= u )
given x being Element of A such that A1: x in B and
A2: f . x [= u ; ::_thesis: FinMeet (B,f) [= u
reconsider u9 = u as Element of (L .:) ;
reconsider f9 = f as Function of A, the carrier of (L .:) ;
 u9 [= f9 . x by A2, Th38;
then  u9 [= FinJoin (B,f9) by A1, Th29;
hence  FinMeet (B,f) [= u by Th39; ::_thesis: verum
end;

theorem :: LATTICE2:42
for L being Lattice
for u being Element of L
for A being non empty set
for B being Finite_Subset of A
for f being Function of A, the carrier of L st ( for x being Element of A st x in B holds
f . x = u ) & B <> {} holds
FinMeet (B,f) = u by SETWISEO:24;

theorem :: LATTICE2:43
for L being Lattice
for v being Element of L
for A being non empty set
for B being Finite_Subset of A
for f being Function of A, the carrier of L st B <> {} holds
v "/\" (FinMeet (B,f)) = FinMeet (B,( the L_meet of L [;] (v,f))) by Th25, SETWISEO:27;

theorem :: LATTICE2:44
for L being Lattice
for u being Element of L
for A being non empty set
for B being Finite_Subset of A
for f being Function of A, the carrier of L st u [= FinMeet (B,f) holds
for x being Element of A st x in B holds
u [= f . x
proof
let L be Lattice; ::_thesis: for u being Element of L
for A being non empty set
for B being Finite_Subset of A
for f being Function of A, the carrier of L st u [= FinMeet (B,f) holds
for x being Element of A st x in B holds
u [= f . x
let u be Element of L; ::_thesis: for A being non empty set
for B being Finite_Subset of A
for f being Function of A, the carrier of L st u [= FinMeet (B,f) holds
for x being Element of A st x in B holds
u [= f . x
let A be non empty set ; ::_thesis: for B being Finite_Subset of A
for f being Function of A, the carrier of L st u [= FinMeet (B,f) holds
for x being Element of A st x in B holds
u [= f . x
let B be Finite_Subset of A; ::_thesis: for f being Function of A, the carrier of L st u [= FinMeet (B,f) holds
for x being Element of A st x in B holds
u [= f . x
let f be Function of A, the carrier of L; ::_thesis: ( u [= FinMeet (B,f) implies for x being Element of A st x in B holds
u [= f . x )
assume A1: u [= FinMeet (B,f) ; ::_thesis: for x being Element of A st x in B holds
u [= f . x
let x be Element of A; ::_thesis: ( x in B implies u [= f . x )
assume  x in B ; ::_thesis: u [= f . x
then  FinMeet (B,f) [= f . x by Th40;
hence  u [= f . x by A1, LATTICES:7; ::_thesis: verum
end;

theorem :: LATTICE2:45
for L being Lattice
for A being non empty set
for B being Finite_Subset of A
for f, g being Function of A, the carrier of L st B <> {} & f | B = g | B holds
FinMeet (B,f) = FinMeet (B,g)
proof
let L be Lattice; ::_thesis: for A being non empty set
for B being Finite_Subset of A
for f, g being Function of A, the carrier of L st B <> {} & f | B = g | B holds
FinMeet (B,f) = FinMeet (B,g)
let A be non empty set ; ::_thesis: for B being Finite_Subset of A
for f, g being Function of A, the carrier of L st B <> {} & f | B = g | B holds
FinMeet (B,f) = FinMeet (B,g)
let B be Finite_Subset of A; ::_thesis: for f, g being Function of A, the carrier of L st B <> {} & f | B = g | B holds
FinMeet (B,f) = FinMeet (B,g)
let f, g be Function of A, the carrier of L; ::_thesis: ( B <> {} & f | B = g | B implies FinMeet (B,f) = FinMeet (B,g) )
reconsider f9 = f, g9 = g as Function of A, the carrier of (L .:) ;
A1: ( FinMeet (B,f) = FinJoin (B,f9) & FinMeet (B,g) = FinJoin (B,g9) ) ;
assume  ( B <> {} & f | B = g | B ) ; ::_thesis: FinMeet (B,f) = FinMeet (B,g)
hence  FinMeet (B,f) = FinMeet (B,g) by A1, Th34; ::_thesis: verum
end;

theorem Th46: :: LATTICE2:46
for L being Lattice
for u being Element of L
for A being non empty set
for B being Finite_Subset of A
for f being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds
u [= f . x ) holds
u [= FinMeet (B,f)
proof
let L be Lattice; ::_thesis: for u being Element of L
for A being non empty set
for B being Finite_Subset of A
for f being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds
u [= f . x ) holds
u [= FinMeet (B,f)
let u be Element of L; ::_thesis: for A being non empty set
for B being Finite_Subset of A
for f being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds
u [= f . x ) holds
u [= FinMeet (B,f)
let A be non empty set ; ::_thesis: for B being Finite_Subset of A
for f being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds
u [= f . x ) holds
u [= FinMeet (B,f)
let B be Finite_Subset of A; ::_thesis: for f being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds
u [= f . x ) holds
u [= FinMeet (B,f)
let f be Function of A, the carrier of L; ::_thesis: ( B <> {} & ( for x being Element of A st x in B holds
u [= f . x ) implies u [= FinMeet (B,f) )
assume that
A1: B <> {} and
A2: for x being Element of A st x in B holds
u [= f . x ; ::_thesis: u [= FinMeet (B,f)
reconsider u9 = u as Element of (L .:) ;
reconsider f9 = f as Function of A, the carrier of (L .:) ;
 for x being Element of A st x in B holds
f9 . x [= u9 by A2, Th38;
then  FinJoin (B,f9) [= u9 by A1, Th32;
hence  u [= FinMeet (B,f) by Th39; ::_thesis: verum
end;

theorem :: LATTICE2:47
for L being Lattice
for A being non empty set
for B being Finite_Subset of A
for f, g being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds
f . x [= g . x ) holds
FinMeet (B,f) [= FinMeet (B,g)
proof
let L be Lattice; ::_thesis: for A being non empty set
for B being Finite_Subset of A
for f, g being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds
f . x [= g . x ) holds
FinMeet (B,f) [= FinMeet (B,g)
let A be non empty set ; ::_thesis: for B being Finite_Subset of A
for f, g being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds
f . x [= g . x ) holds
FinMeet (B,f) [= FinMeet (B,g)
let B be Finite_Subset of A; ::_thesis: for f, g being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds
f . x [= g . x ) holds
FinMeet (B,f) [= FinMeet (B,g)
let f, g be Function of A, the carrier of L; ::_thesis: ( B <> {} & ( for x being Element of A st x in B holds
f . x [= g . x ) implies FinMeet (B,f) [= FinMeet (B,g) )
assume that
A1: B <> {} and
A2: for x being Element of A st x in B holds
f . x [= g . x ; ::_thesis: FinMeet (B,f) [= FinMeet (B,g)
now__::_thesis:_for_x_being_Element_of_A_st_x_in_B_holds_
FinMeet_(B,f)_[=_g_._x
let x be Element of A; ::_thesis: ( x in B implies FinMeet (B,f) [= g . x )
assume A3: x in B ; ::_thesis: FinMeet (B,f) [= g . x
then  f . x [= g . x by A2;
hence  FinMeet (B,f) [= g . x by A3, Th41; ::_thesis: verum
end;
hence  FinMeet (B,f) [= FinMeet (B,g) by A1, Th46; ::_thesis: verum
end;

theorem :: LATTICE2:48
for L being Lattice holds
( L is lower-bounded iff L .: is upper-bounded )
proof
let L be Lattice; ::_thesis: ( L is lower-bounded iff L .: is upper-bounded )
thus  ( L is lower-bounded implies L .: is upper-bounded ) ::_thesis: ( L .: is upper-bounded implies L is lower-bounded )
proof
given c being Element of L such that A1: for a being Element of L holds
( c "/\" a = c & a "/\" c = c ) ; :: according to LATTICES:def_13 ::_thesis: L .: is upper-bounded
reconsider c9 = c as Element of (L .:) ;
take  c9 ; :: according to LATTICES:def_14 ::_thesis: for b1 being Element of the carrier of (L .:) holds
( c9 "\/" b1 = c9 & b1 "\/" c9 = c9 )
let a9 be Element of (L .:); ::_thesis: ( c9 "\/" a9 = c9 & a9 "\/" c9 = c9 )
reconsider a = a9 as Element of L ;
thus c9 "\/" a9 = c "/\" a
.= c9 by A1 ; ::_thesis: a9 "\/" c9 = c9
hence  a9 "\/" c9 = c9 ; ::_thesis: verum
end;
given c being Element of (L .:) such that A2: for a being Element of (L .:) holds
( c "\/" a = c & a "\/" c = c ) ; :: according to LATTICES:def_14 ::_thesis: L is lower-bounded
reconsider c9 = c as Element of L ;
take  c9 ; :: according to LATTICES:def_13 ::_thesis: for b1 being Element of the carrier of L holds
( c9 "/\" b1 = c9 & b1 "/\" c9 = c9 )
let a9 be Element of L; ::_thesis: ( c9 "/\" a9 = c9 & a9 "/\" c9 = c9 )
reconsider a = a9 as Element of (L .:) ;
thus c9 "/\" a9 = c "\/" a
.= c9 by A2 ; ::_thesis: a9 "/\" c9 = c9
hence  a9 "/\" c9 = c9 ; ::_thesis: verum
end;

theorem Th49: :: LATTICE2:49
for L being Lattice holds
( L is upper-bounded iff L .: is lower-bounded )
proof
let L be Lattice; ::_thesis: ( L is upper-bounded iff L .: is lower-bounded )
thus  ( L is upper-bounded implies L .: is lower-bounded ) ::_thesis: ( L .: is lower-bounded implies L is upper-bounded )
proof
given c being Element of L such that A1: for a being Element of L holds
( c "\/" a = c & a "\/" c = c ) ; :: according to LATTICES:def_14 ::_thesis: L .: is lower-bounded
reconsider c9 = c as Element of (L .:) ;
take  c9 ; :: according to LATTICES:def_13 ::_thesis: for b1 being Element of the carrier of (L .:) holds
( c9 "/\" b1 = c9 & b1 "/\" c9 = c9 )
let a9 be Element of (L .:); ::_thesis: ( c9 "/\" a9 = c9 & a9 "/\" c9 = c9 )
reconsider a = a9 as Element of L ;
thus c9 "/\" a9 = c "\/" a
.= c9 by A1 ; ::_thesis: a9 "/\" c9 = c9
hence  a9 "/\" c9 = c9 ; ::_thesis: verum
end;
given c being Element of (L .:) such that A2: for a being Element of (L .:) holds
( c "/\" a = c & a "/\" c = c ) ; :: according to LATTICES:def_13 ::_thesis: L is upper-bounded
reconsider c9 = c as Element of L ;
take  c9 ; :: according to LATTICES:def_14 ::_thesis: for b1 being Element of the carrier of L holds
( c9 "\/" b1 = c9 & b1 "\/" c9 = c9 )
let a9 be Element of L; ::_thesis: ( c9 "\/" a9 = c9 & a9 "\/" c9 = c9 )
reconsider a = a9 as Element of (L .:) ;
thus c9 "\/" a9 = c "/\" a
.= c9 by A2 ; ::_thesis: a9 "\/" c9 = c9
hence  a9 "\/" c9 = c9 ; ::_thesis: verum
end;

theorem :: LATTICE2:50
for L being Lattice holds
( L is D_Lattice iff L .: is D_Lattice ) by Th22, Th23;


theorem Th51: :: LATTICE2:51
for L being 0_Lattice holds Bottom L is_a_unity_wrt the L_join of L
proof
let L be 0_Lattice; ::_thesis: Bottom L is_a_unity_wrt the L_join of L
now__::_thesis:_for_u_being_Element_of_L_holds_the_L_join_of_L_._((Bottom_L),u)_=_u
let u be Element of L; ::_thesis: the L_join of L . ((Bottom L),u) = u
thus  the L_join of L . ((Bottom L),u) = (Bottom L) "\/" u
.= u ; ::_thesis: verum
end;
hence  Bottom L is_a_unity_wrt the L_join of L by BINOP_1:4; ::_thesis: verum
end;

registration
let L be 0_Lattice;
cluster the L_join of L ->  having_a_unity ;
coherence
 the L_join of L is having_a_unity
proof
 Bottom L is_a_unity_wrt the L_join of L by Th51;
hence  the L_join of L is having_a_unity by SETWISEO:def_2; ::_thesis: verum
end;
end;

theorem :: LATTICE2:52
for L being 0_Lattice holds Bottom L = the_unity_wrt the L_join of L by Th18;

theorem Th53: :: LATTICE2:53
for A being non empty set
for B being Finite_Subset of A
for L being 0_Lattice
for f, g being Function of A, the carrier of L st f | B = g | B holds
FinJoin (B,f) = FinJoin (B,g)
proof
let A be non empty set ; ::_thesis: for B being Finite_Subset of A
for L being 0_Lattice
for f, g being Function of A, the carrier of L st f | B = g | B holds
FinJoin (B,f) = FinJoin (B,g)
let B be Finite_Subset of A; ::_thesis: for L being 0_Lattice
for f, g being Function of A, the carrier of L st f | B = g | B holds
FinJoin (B,f) = FinJoin (B,g)
let L be 0_Lattice; ::_thesis: for f, g being Function of A, the carrier of L st f | B = g | B holds
FinJoin (B,f) = FinJoin (B,g)
let f, g be Function of A, the carrier of L; ::_thesis: ( f | B = g | B implies FinJoin (B,f) = FinJoin (B,g) )
set J = the L_join of L;
A1: Bottom L = the_unity_wrt the L_join of L by Th18;
assume A2: f | B = g | B ; ::_thesis: FinJoin (B,f) = FinJoin (B,g)
now__::_thesis:_FinJoin_(B,f)_=_FinJoin_(B,g)
percases ( B = {} or B <> {} ) ;
supposeA3: B = {} ; ::_thesis: FinJoin (B,f) = FinJoin (B,g)
hence  FinJoin (B,f) = the L_join of L $$ (({}. A),f)
.= Bottom L by A1, SETWISEO:31
.= the L_join of L $$ (({}. A),g) by A1, SETWISEO:31
.= FinJoin (B,g) by A3 ;
::_thesis: verum
end;
suppose B <> {} ; ::_thesis: FinJoin (B,f) = FinJoin (B,g)
hence  FinJoin (B,f) = FinJoin (B,g) by A2, Th34; ::_thesis: verum
end;
end;
end;
hence  FinJoin (B,f) = FinJoin (B,g) ; ::_thesis: verum
end;

theorem Th54: :: LATTICE2:54
for A being non empty set
for B being Finite_Subset of A
for L being 0_Lattice
for f being Function of A, the carrier of L
for u being Element of L st ( for x being Element of A st x in B holds
f . x [= u ) holds
FinJoin (B,f) [= u
proof
let A be non empty set ; ::_thesis: for B being Finite_Subset of A
for L being 0_Lattice
for f being Function of A, the carrier of L
for u being Element of L st ( for x being Element of A st x in B holds
f . x [= u ) holds
FinJoin (B,f) [= u
let B be Finite_Subset of A; ::_thesis: for L being 0_Lattice
for f being Function of A, the carrier of L
for u being Element of L st ( for x being Element of A st x in B holds
f . x [= u ) holds
FinJoin (B,f) [= u
let L be 0_Lattice; ::_thesis: for f being Function of A, the carrier of L
for u being Element of L st ( for x being Element of A st x in B holds
f . x [= u ) holds
FinJoin (B,f) [= u
let f be Function of A, the carrier of L; ::_thesis: for u being Element of L st ( for x being Element of A st x in B holds
f . x [= u ) holds
FinJoin (B,f) [= u
let u be Element of L; ::_thesis: ( ( for x being Element of A st x in B holds
f . x [= u ) implies FinJoin (B,f) [= u )
assume A1: for x being Element of A st x in B holds
f . x [= u ; ::_thesis: FinJoin (B,f) [= u
set J = the L_join of L;
A2: Bottom L = the_unity_wrt the L_join of L by Th18;
now__::_thesis:_FinJoin_(B,f)_[=_u
percases ( B = {} or B <> {} ) ;
suppose B = {} ; ::_thesis: FinJoin (B,f) [= u
then  FinJoin (B,f) = the L_join of L $$ (({}. A),f)
.= Bottom L by A2, SETWISEO:31 ;
hence  FinJoin (B,f) [= u by LATTICES:16; ::_thesis: verum
end;
suppose B <> {} ; ::_thesis: FinJoin (B,f) [= u
hence  FinJoin (B,f) [= u by A1, Th32; ::_thesis: verum
end;
end;
end;
hence  FinJoin (B,f) [= u ; ::_thesis: verum
end;

theorem :: LATTICE2:55
for A being non empty set
for B being Finite_Subset of A
for L being 0_Lattice
for f, g being Function of A, the carrier of L st ( for x being Element of A st x in B holds
f . x [= g . x ) holds
FinJoin (B,f) [= FinJoin (B,g)
proof
let A be non empty set ; ::_thesis: for B being Finite_Subset of A
for L being 0_Lattice
for f, g being Function of A, the carrier of L st ( for x being Element of A st x in B holds
f . x [= g . x ) holds
FinJoin (B,f) [= FinJoin (B,g)
let B be Finite_Subset of A; ::_thesis: for L being 0_Lattice
for f, g being Function of A, the carrier of L st ( for x being Element of A st x in B holds
f . x [= g . x ) holds
FinJoin (B,f) [= FinJoin (B,g)
let L be 0_Lattice; ::_thesis: for f, g being Function of A, the carrier of L st ( for x being Element of A st x in B holds
f . x [= g . x ) holds
FinJoin (B,f) [= FinJoin (B,g)
let f, g be Function of A, the carrier of L; ::_thesis: ( ( for x being Element of A st x in B holds
f . x [= g . x ) implies FinJoin (B,f) [= FinJoin (B,g) )
assume A1: for x being Element of A st x in B holds
f . x [= g . x ; ::_thesis: FinJoin (B,f) [= FinJoin (B,g)
now__::_thesis:_for_x_being_Element_of_A_st_x_in_B_holds_
f_._x_[=_FinJoin_(B,g)
let x be Element of A; ::_thesis: ( x in B implies f . x [= FinJoin (B,g) )
assume A2: x in B ; ::_thesis: f . x [= FinJoin (B,g)
then  f . x [= g . x by A1;
hence  f . x [= FinJoin (B,g) by A2, Th29; ::_thesis: verum
end;
hence  FinJoin (B,f) [= FinJoin (B,g) by Th54; ::_thesis: verum
end;


theorem Th56: :: LATTICE2:56
for L being 1_Lattice holds Top L is_a_unity_wrt the L_meet of L
proof
let L be 1_Lattice; ::_thesis: Top L is_a_unity_wrt the L_meet of L
now__::_thesis:_for_u_being_Element_of_L_holds_the_L_meet_of_L_._((Top_L),u)_=_u
let u be Element of L; ::_thesis: the L_meet of L . ((Top L),u) = u
thus  the L_meet of L . ((Top L),u) = (Top L) "/\" u
.= u ; ::_thesis: verum
end;
hence  Top L is_a_unity_wrt the L_meet of L by BINOP_1:4; ::_thesis: verum
end;

registration
let L be 1_Lattice;
cluster the L_meet of L ->  having_a_unity ;
coherence
 the L_meet of L is having_a_unity
proof
 Top L is_a_unity_wrt the L_meet of L by Th56;
hence  the L_meet of L is having_a_unity by SETWISEO:def_2; ::_thesis: verum
end;
end;

theorem :: LATTICE2:57
for L being 1_Lattice holds Top L = the_unity_wrt the L_meet of L by Th19;

theorem :: LATTICE2:58
for A being non empty set
for B being Finite_Subset of A
for L being 1_Lattice
for f, g being Function of A, the carrier of L st f | B = g | B holds
FinMeet (B,f) = FinMeet (B,g)
proof
let A be non empty set ; ::_thesis: for B being Finite_Subset of A
for L being 1_Lattice
for f, g being Function of A, the carrier of L st f | B = g | B holds
FinMeet (B,f) = FinMeet (B,g)
let B be Finite_Subset of A; ::_thesis: for L being 1_Lattice
for f, g being Function of A, the carrier of L st f | B = g | B holds
FinMeet (B,f) = FinMeet (B,g)
let L be 1_Lattice; ::_thesis: for f, g being Function of A, the carrier of L st f | B = g | B holds
FinMeet (B,f) = FinMeet (B,g)
let f, g be Function of A, the carrier of L; ::_thesis: ( f | B = g | B implies FinMeet (B,f) = FinMeet (B,g) )
assume A1: f | B = g | B ; ::_thesis: FinMeet (B,f) = FinMeet (B,g)
reconsider f9 = f, g9 = g as Function of A, the carrier of (L .:) ;
A2: FinMeet (B,g) = FinJoin (B,g9) ;
 ( L .: is 0_Lattice & FinMeet (B,f) = FinJoin (B,f9) ) by Th49;
hence  FinMeet (B,f) = FinMeet (B,g) by A1, A2, Th53; ::_thesis: verum
end;

theorem Th59: :: LATTICE2:59
for A being non empty set
for B being Finite_Subset of A
for L being 1_Lattice
for f being Function of A, the carrier of L
for u being Element of L st ( for x being Element of A st x in B holds
u [= f . x ) holds
u [= FinMeet (B,f)
proof
let A be non empty set ; ::_thesis: for B being Finite_Subset of A
for L being 1_Lattice
for f being Function of A, the carrier of L
for u being Element of L st ( for x being Element of A st x in B holds
u [= f . x ) holds
u [= FinMeet (B,f)
let B be Finite_Subset of A; ::_thesis: for L being 1_Lattice
for f being Function of A, the carrier of L
for u being Element of L st ( for x being Element of A st x in B holds
u [= f . x ) holds
u [= FinMeet (B,f)
let L be 1_Lattice; ::_thesis: for f being Function of A, the carrier of L
for u being Element of L st ( for x being Element of A st x in B holds
u [= f . x ) holds
u [= FinMeet (B,f)
let f be Function of A, the carrier of L; ::_thesis: for u being Element of L st ( for x being Element of A st x in B holds
u [= f . x ) holds
u [= FinMeet (B,f)
let u be Element of L; ::_thesis: ( ( for x being Element of A st x in B holds
u [= f . x ) implies u [= FinMeet (B,f) )
reconsider f9 = f as Function of A, the carrier of (L .:) ;
reconsider u9 = u as Element of (L .:) ;
assume  for x being Element of A st x in B holds
u [= f . x ; ::_thesis: u [= FinMeet (B,f)
then A1: for x being Element of A st x in B holds
f9 . x [= u9 by Th38;
 L .: is 0_Lattice by Th49;
then  FinJoin (B,f9) [= u9 by A1, Th54;
hence  u [= FinMeet (B,f) by Th39; ::_thesis: verum
end;

theorem :: LATTICE2:60
for A being non empty set
for B being Finite_Subset of A
for L being 1_Lattice
for f, g being Function of A, the carrier of L st ( for x being Element of A st x in B holds
f . x [= g . x ) holds
FinMeet (B,f) [= FinMeet (B,g)
proof
let A be non empty set ; ::_thesis: for B being Finite_Subset of A
for L being 1_Lattice
for f, g being Function of A, the carrier of L st ( for x being Element of A st x in B holds
f . x [= g . x ) holds
FinMeet (B,f) [= FinMeet (B,g)
let B be Finite_Subset of A; ::_thesis: for L being 1_Lattice
for f, g being Function of A, the carrier of L st ( for x being Element of A st x in B holds
f . x [= g . x ) holds
FinMeet (B,f) [= FinMeet (B,g)
let L be 1_Lattice; ::_thesis: for f, g being Function of A, the carrier of L st ( for x being Element of A st x in B holds
f . x [= g . x ) holds
FinMeet (B,f) [= FinMeet (B,g)
let f, g be Function of A, the carrier of L; ::_thesis: ( ( for x being Element of A st x in B holds
f . x [= g . x ) implies FinMeet (B,f) [= FinMeet (B,g) )
assume A1: for x being Element of A st x in B holds
f . x [= g . x ; ::_thesis: FinMeet (B,f) [= FinMeet (B,g)
now__::_thesis:_for_x_being_Element_of_A_st_x_in_B_holds_
FinMeet_(B,f)_[=_g_._x
let x be Element of A; ::_thesis: ( x in B implies FinMeet (B,f) [= g . x )
assume A2: x in B ; ::_thesis: FinMeet (B,f) [= g . x
then  f . x [= g . x by A1;
hence  FinMeet (B,f) [= g . x by A2, Th41; ::_thesis: verum
end;
hence  FinMeet (B,f) [= FinMeet (B,g) by Th59; ::_thesis: verum
end;

theorem :: LATTICE2:61
for L being 0_Lattice holds Bottom L = Top (L .:)
proof
let L be 0_Lattice; ::_thesis: Bottom L = Top (L .:)
reconsider u = Bottom L as Element of (L .:) ;
now__::_thesis:_for_v_being_Element_of_(L_.:)_holds_v_"\/"_u_=_u
let v be Element of (L .:); ::_thesis: v "\/" u = u
reconsider v9 = v as Element of L ;
thus v "\/" u = (Bottom L) "/\" v9 by Th37
.= u ; ::_thesis: verum
end;
hence  Bottom L = Top (L .:) by RLSUB_2:65; ::_thesis: verum
end;

theorem :: LATTICE2:62
for L being 1_Lattice holds Top L = Bottom (L .:)
proof
let L be 1_Lattice; ::_thesis: Top L = Bottom (L .:)
reconsider u = Top L as Element of (L .:) ;
now__::_thesis:_for_v_being_Element_of_(L_.:)_holds_v_"/\"_u_=_u
let v be Element of (L .:); ::_thesis: v "/\" u = u
reconsider v9 = v as Element of L ;
thus v "/\" u = (Top L) "\/" v9 by Th37
.= u ; ::_thesis: verum
end;
hence  Top L = Bottom (L .:) by RLSUB_2:64; ::_thesis: verum
end;

definition
mode D0_Lattice is distributive lower-bounded Lattice;
end;


theorem :: LATTICE2:63
for L being D0_Lattice holds the L_meet of L is_distributive_wrt the L_join of L by Th23;

theorem Th64: :: LATTICE2:64
for A being non empty set
for B being Finite_Subset of A
for L being D0_Lattice
for f being Function of A, the carrier of L
for u being Element of L holds the L_meet of L . (u,(FinJoin (B,f))) = FinJoin (B,( the L_meet of L [;] (u,f)))
proof
let A be non empty set ; ::_thesis: for B being Finite_Subset of A
for L being D0_Lattice
for f being Function of A, the carrier of L
for u being Element of L holds the L_meet of L . (u,(FinJoin (B,f))) = FinJoin (B,( the L_meet of L [;] (u,f)))
let B be Finite_Subset of A; ::_thesis: for L being D0_Lattice
for f being Function of A, the carrier of L
for u being Element of L holds the L_meet of L . (u,(FinJoin (B,f))) = FinJoin (B,( the L_meet of L [;] (u,f)))
let L be D0_Lattice; ::_thesis: for f being Function of A, the carrier of L
for u being Element of L holds the L_meet of L . (u,(FinJoin (B,f))) = FinJoin (B,( the L_meet of L [;] (u,f)))
let f be Function of A, the carrier of L; ::_thesis: for u being Element of L holds the L_meet of L . (u,(FinJoin (B,f))) = FinJoin (B,( the L_meet of L [;] (u,f)))
let u be Element of L; ::_thesis: the L_meet of L . (u,(FinJoin (B,f))) = FinJoin (B,( the L_meet of L [;] (u,f)))
A1: the L_meet of L . (u,(Bottom L)) = u "/\" (Bottom L)
.= Bottom L ;
 ( the L_meet of L is_distributive_wrt the L_join of L & Bottom L = the_unity_wrt the L_join of L ) by Th18, Th23;
hence  the L_meet of L . (u,(FinJoin (B,f))) = FinJoin (B,( the L_meet of L [;] (u,f))) by A1, SETWOP_2:12; ::_thesis: verum
end;

theorem :: LATTICE2:65
for A being non empty set
for B being Finite_Subset of A
for L being D0_Lattice
for g, f being Function of A, the carrier of L
for u being Element of L st ( for x being Element of A st x in B holds
g . x = u "/\" (f . x) ) holds
u "/\" (FinJoin (B,f)) = FinJoin (B,g)
proof
let A be non empty set ; ::_thesis: for B being Finite_Subset of A
for L being D0_Lattice
for g, f being Function of A, the carrier of L
for u being Element of L st ( for x being Element of A st x in B holds
g . x = u "/\" (f . x) ) holds
u "/\" (FinJoin (B,f)) = FinJoin (B,g)
let B be Finite_Subset of A; ::_thesis: for L being D0_Lattice
for g, f being Function of A, the carrier of L
for u being Element of L st ( for x being Element of A st x in B holds
g . x = u "/\" (f . x) ) holds
u "/\" (FinJoin (B,f)) = FinJoin (B,g)
let L be D0_Lattice; ::_thesis: for g, f being Function of A, the carrier of L
for u being Element of L st ( for x being Element of A st x in B holds
g . x = u "/\" (f . x) ) holds
u "/\" (FinJoin (B,f)) = FinJoin (B,g)
let g, f be Function of A, the carrier of L; ::_thesis: for u being Element of L st ( for x being Element of A st x in B holds
g . x = u "/\" (f . x) ) holds
u "/\" (FinJoin (B,f)) = FinJoin (B,g)
let u be Element of L; ::_thesis: ( ( for x being Element of A st x in B holds
g . x = u "/\" (f . x) ) implies u "/\" (FinJoin (B,f)) = FinJoin (B,g) )
reconsider G = ( the L_meet of L [;] (u,f)) +* (g | B) as Function of A, the carrier of L by Th3;
 dom (g | B) = B by Th9;
then A1: G | B = g | B by FUNCT_4:23;
assume A2: for x being Element of A st x in B holds
g . x = u "/\" (f . x) ; ::_thesis: u "/\" (FinJoin (B,f)) = FinJoin (B,g)
now__::_thesis:_for_x_being_Element_of_A_st_x_in_B_holds_
g_._x_=_(_the_L_meet_of_L_[;]_(u,f))_._x
let x be Element of A; ::_thesis: ( x in B implies g . x = ( the L_meet of L [;] (u,f)) . x )
assume  x in B ; ::_thesis: g . x = ( the L_meet of L [;] (u,f)) . x
hence g . x = u "/\" (f . x) by A2
.= ( the L_meet of L [;] (u,f)) . x by FUNCOP_1:53 ;
::_thesis: verum
end;
then  G = the L_meet of L [;] (u,f) by Th10;
hence u "/\" (FinJoin (B,f)) = FinJoin (B,G) by Th64
.= FinJoin (B,g) by A1, Th53 ;
::_thesis: verum
end;

theorem :: LATTICE2:66
for A being non empty set
for B being Finite_Subset of A
for L being D0_Lattice
for f being Function of A, the carrier of L
for u being Element of L holds u "/\" (FinJoin (B,f)) = FinJoin (B,( the L_meet of L [;] (u,f))) by Th64;

definition
let IT be Lattice;
attrIT is Heyting  means :Def5: :: LATTICE2:def 5
( IT is implicative & IT is lower-bounded );
end;

:: deftheorem Def5 defines Heyting LATTICE2:def_5_:_
 for IT being Lattice holds
( IT is Heyting iff ( IT is implicative & IT is lower-bounded ) );

registration
cluster non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like Heyting for LattStr ;
existence
 ex b1 being Lattice st b1 is Heyting
proof
set L = the B_Lattice;
take  the B_Lattice ; ::_thesis: the B_Lattice is Heyting
thus  ( the B_Lattice is implicative & the B_Lattice is lower-bounded ) ; :: according to LATTICE2:def_5 ::_thesis: verum
end;
end;

registration
cluster non empty Lattice-like Heyting  ->  lower-bounded implicative for LattStr ;
coherence
 for b1 being Lattice st b1 is Heyting holds
( b1 is implicative & b1 is lower-bounded ) by Def5;
cluster non empty Lattice-like lower-bounded implicative  ->  Heyting for LattStr ;
coherence
 for b1 being Lattice st b1 is implicative & b1 is lower-bounded holds
b1 is Heyting by Def5;
end;

definition
mode H_Lattice is Heyting Lattice;
end;

registration
cluster non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like Heyting for LattStr ;
existence
 ex b1 being Lattice st
( b1 is Heyting & b1 is strict )
proof
set L = the strict B_Lattice;
 the strict B_Lattice is I_Lattice ;
hence  ex b1 being Lattice st
( b1 is Heyting & b1 is strict ) ; ::_thesis: verum
end;
end;

theorem :: LATTICE2:67
for L being 0_Lattice holds
( L is H_Lattice iff for x, z being Element of L ex y being Element of L st
( x "/\" y [= z & ( for v being Element of L st x "/\" v [= z holds
v [= y ) ) )
proof
let L be 0_Lattice; ::_thesis: ( L is H_Lattice iff for x, z being Element of L ex y being Element of L st
( x "/\" y [= z & ( for v being Element of L st x "/\" v [= z holds
v [= y ) ) )
 ( L is H_Lattice iff L is I_Lattice ) ;
hence  ( L is H_Lattice iff for x, z being Element of L ex y being Element of L st
( x "/\" y [= z & ( for v being Element of L st x "/\" v [= z holds
v [= y ) ) ) by FILTER_0:def_6; ::_thesis: verum
end;

theorem :: LATTICE2:68
for L being Lattice holds
( L is finite iff L .: is finite ) ;

registration
cluster non empty finite Lattice-like  ->  lower-bounded for LattStr ;
coherence
 for b1 being Lattice st b1 is finite holds
b1 is lower-bounded
proof
let L be Lattice; ::_thesis: ( L is finite implies L is lower-bounded )
assume  L is finite ; ::_thesis: L is lower-bounded
then reconsider B = the carrier of L as Finite_Subset of the carrier of L by FINSUB_1:def_5;
take c = FinMeet (B,(id the carrier of L)); :: according to LATTICES:def_13 ::_thesis: for b1 being Element of the carrier of L holds
( c "/\" b1 = c & b1 "/\" c = c )
let a be Element of L; ::_thesis: ( c "/\" a = c & a "/\" c = c )
 (id the carrier of L) . a [= a by FUNCT_1:18;
then A1: c [= a by Th41;
hence  c "/\" a = c by LATTICES:4; ::_thesis: a "/\" c = c
thus  a "/\" c = c by A1, LATTICES:4; ::_thesis: verum
end;
cluster non empty finite Lattice-like  ->  upper-bounded for LattStr ;
coherence
 for b1 being Lattice st b1 is finite holds
b1 is upper-bounded
proof
let L be Lattice; ::_thesis: ( L is finite implies L is upper-bounded )
assume  L is finite ; ::_thesis: L is upper-bounded
then reconsider B = the carrier of L as Finite_Subset of the carrier of L by FINSUB_1:def_5;
take c = FinJoin (B,(id the carrier of L)); :: according to LATTICES:def_14 ::_thesis: for b1 being Element of the carrier of L holds
( c "\/" b1 = c & b1 "\/" c = c )
let a be Element of L; ::_thesis: ( c "\/" a = c & a "\/" c = c )
 a [= (id the carrier of L) . a by FUNCT_1:18;
then A2: a [= c by Th29;
hence  c "\/" a = c by LATTICES:def_3; ::_thesis: a "\/" c = c
thus  a "\/" c = c by A2, LATTICES:def_3; ::_thesis: verum
end;
end;

registration
cluster non empty finite Lattice-like  ->  bounded for LattStr ;
coherence
 for b1 being Lattice st b1 is finite holds
b1 is bounded ;
end;

registration
cluster non empty finite Lattice-like distributive  ->  Heyting for LattStr ;
coherence
 for b1 being Lattice st b1 is distributive & b1 is finite holds
b1 is Heyting
proof
let L be Lattice; ::_thesis: ( L is distributive & L is finite implies L is Heyting )
assume A1: ( L is distributive & L is finite ) ; ::_thesis: L is Heyting
then reconsider L = L as D0_Lattice ;
set C = the carrier of L;
 L is implicative
proof
let p, q be Element of the carrier of L; :: according to FILTER_0:def_6 ::_thesis: ex b1 being Element of the carrier of L st
( p "/\" b1 [= q & ( for b2 being Element of the carrier of L holds
( not p "/\" b2 [= q or b2 [= b1 ) ) )
defpred S1[ Element of the carrier of L] means p "/\" c1 [= q;
set B =  {  x where x is Element of the carrier of L : S1[x]  }  ;
A2:  {  x where x is Element of the carrier of L : S1[x]  }  c= the carrier of L from FRAENKEL:sch_10();
then   {  x where x is Element of the carrier of L : S1[x]  }  is finite by A1, FINSET_1:1;
then reconsider B =  {  x where x is Element of the carrier of L : S1[x]  }  as Finite_Subset of the carrier of L by A2, FINSUB_1:def_5;
take r = FinJoin (B,(id the carrier of L)); ::_thesis: ( p "/\" r [= q & ( for b1 being Element of the carrier of L holds
( not p "/\" b1 [= q or b1 [= r ) ) )
A3: now__::_thesis:_for_x_being_Element_of_the_carrier_of_L_st_x_in_B_holds_
(_the_L_meet_of_L_[;]_(p,(id_the_carrier_of_L)))_._x_[=_q
let x be Element of the carrier of L; ::_thesis: ( x in B implies ( the L_meet of L [;] (p,(id the carrier of L))) . x [= q )
assume  x in B ; ::_thesis: ( the L_meet of L [;] (p,(id the carrier of L))) . x [= q
then A4: ex x9 being Element of the carrier of L st
( x9 = x & p "/\" x9 [= q ) ;
( the L_meet of L [;] (p,(id the carrier of L))) . x = the L_meet of L . (p,((id the carrier of L) . x)) by FUNCOP_1:53
.= p "/\" x by FUNCT_1:18 ;
hence  ( the L_meet of L [;] (p,(id the carrier of L))) . x [= q by A4; ::_thesis: verum
end;
 p "/\" r = FinJoin (B,( the L_meet of L [;] (p,(id the carrier of L)))) by Th64;
hence  p "/\" r [= q by A3, Th54; ::_thesis: for b1 being Element of the carrier of L holds
( not p "/\" b1 [= q or b1 [= r )
let r1 be Element of the carrier of L; ::_thesis: ( not p "/\" r1 [= q or r1 [= r )
assume  p "/\" r1 [= q ; ::_thesis: r1 [= r
then A5: r1 in B ;
 r1 = (id the carrier of L) . r1 by FUNCT_1:18;
hence  r1 [= r by A5, Th28; ::_thesis: verum
end;
hence  L is Heyting ; ::_thesis: verum
end;
end;