:: Filters - Part I. Implicative Lattices
:: by Grzegorz Bancerek
::
:: Received July 3, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

theorem Th1: :: FILTER_0:1
for L being non empty join-commutative join-associative meet-commutative meet-absorbing join-absorbing LattStr
for p, q, r being Element of L st p [= q holds
r "\/" p [= r "\/" q
proofend;

theorem :: FILTER_0:2
for L being Lattice
for p, r, q being Element of L st p [= r holds
p "/\" q [= r
proofend;

theorem :: FILTER_0:3
for L being Lattice
for p, r, q being Element of L st p [= r holds
p [= q "\/" r
proofend;

theorem Th4: :: FILTER_0:4
for L being non empty join-commutative join-associative join-absorbing LattStr
for a, b, c, d being Element of L st a [= b & c [= d holds
a "\/" c [= b "\/" d
proofend;

theorem Th5: :: FILTER_0:5
for L being non empty meet-commutative meet-associative meet-absorbing join-absorbing LattStr
for a, b, c, d being Element of L st a [= b & c [= d holds
a "/\" c [= b "/\" d
proofend;

theorem Th6: :: FILTER_0:6
for L being non empty join-commutative join-associative meet-commutative meet-absorbing join-absorbing LattStr
for a, b, c being Element of L st a [= c & b [= c holds
a "\/" b [= c
proofend;

theorem Th7: :: FILTER_0:7
for L being non empty meet-commutative meet-associative meet-absorbing join-absorbing LattStr
for a, b, c being Element of L st a [= b & a [= c holds
a [= b "/\" c
proofend;

definition
let L be Lattice;
mode Filter of L is non empty final meet-closed Subset of L;
end;

theorem Th8: :: FILTER_0:8
for L being Lattice
for S being non empty Subset of L holds
( S is Filter of L iff for p, q being Element of L holds
( ( p in S & q in S ) iff p "/\" q in S ) )
proofend;

theorem Th9: :: FILTER_0:9
for L being Lattice
for D being non empty Subset of L holds
( D is Filter of L iff ( ( for p, q being Element of L st p in D & q in D holds
p "/\" q in D ) & ( for p, q being Element of L st p in D & p [= q holds
q in D ) ) )
proofend;

theorem Th10: :: FILTER_0:10
for L being Lattice
for p, q being Element of L
for H being Filter of L st p in H holds
( p "\/" q in H & q "\/" p in H )
proofend;

theorem Th11: :: FILTER_0:11
for L being Lattice
for H being Filter of L st L is 1_Lattice holds
Top L in H
proofend;

theorem :: FILTER_0:12
for L being Lattice st L is 1_Lattice holds
{(Top L)} is Filter of L
proofend;

theorem :: FILTER_0:13
for L being Lattice
for p being Element of L st {p} is Filter of L holds
L is upper-bounded
proofend;

theorem Th14: :: FILTER_0:14
for L being Lattice holds the carrier of L is Filter of L
proofend;

definition
let L be Lattice;
func<.L.) ->  Filter of L equals :: FILTER_0:def 1
 the carrier of L;
coherence
 the carrier of L is Filter of L by Th14;
end;

:: deftheorem  defines <. FILTER_0:def_1_:_
 for L being Lattice holds <.L.) = the carrier of L;

definition
let L be Lattice;
let p be Element of L;
func<.p.) ->  Filter of L equals :: FILTER_0:def 2
 {  q where q is Element of L : p [= q  }  ;
coherence
  {  q where q is Element of L : p [= q  }  is Filter of L
proofend;
end;

:: deftheorem  defines <. FILTER_0:def_2_:_
 for L being Lattice
for p being Element of L holds <.p.) =  {  q where q is Element of L : p [= q  }  ;

theorem Th15: :: FILTER_0:15
for L being Lattice
for q, p being Element of L holds
( q in <.p.) iff p [= q )
proofend;

theorem Th16: :: FILTER_0:16
for L being Lattice
for p, q being Element of L holds
( p in <.p.) &amp; p "\/" q in <.p.) &amp; q "\/" p in <.p.) )
proofend;

theorem Th17: :: FILTER_0:17
for L being Lattice st L is 0_Lattice holds
<.L.) = <.(Bottom L).)
proofend;

definition
let L be Lattice;
let F be Filter of L;
attrF is being_ultrafilter  means :Def3: :: FILTER_0:def 3
( F <> the carrier of L &amp; ( for H being Filter of L st F c= H &amp; H <> the carrier of L holds
F = H ) );
end;

:: deftheorem Def3 defines being_ultrafilter FILTER_0:def_3_:_
 for L being Lattice
for F being Filter of L holds
( F is being_ultrafilter iff ( F <> the carrier of L &amp; ( for H being Filter of L st F c= H &amp; H <> the carrier of L holds
F = H ) ) );

theorem Th18: :: FILTER_0:18
for L being Lattice st L is lower-bounded holds
for F being Filter of L st F <> the carrier of L holds
ex H being Filter of L st
( F c= H &amp; H is being_ultrafilter )
proofend;

theorem Th19: :: FILTER_0:19
for L being Lattice
for p being Element of L st ex r being Element of L st p "/\" r <> p holds
<.p.) <> the carrier of L
proofend;

theorem Th20: :: FILTER_0:20
for L being Lattice
for p being Element of L st L is 0_Lattice &amp; p <> Bottom L holds
ex H being Filter of L st
( p in H &amp; H is being_ultrafilter )
proofend;

definition
let L be Lattice;
let D be non empty Subset of L;
func<.D.) ->  Filter of L means :Def4: :: FILTER_0:def 4
( D c= it &amp; ( for F being Filter of L st D c= F holds
it c= F ) );
existence
 ex b1 being Filter of L st
( D c= b1 &amp; ( for F being Filter of L st D c= F holds
b1 c= F ) )
proofend;
uniqueness
 for b1, b2 being Filter of L st D c= b1 &amp; ( for F being Filter of L st D c= F holds
b1 c= F ) &amp; D c= b2 &amp; ( for F being Filter of L st D c= F holds
b2 c= F ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines <. FILTER_0:def_4_:_
 for L being Lattice
for D being non empty Subset of L
for b3 being Filter of L holds
( b3 = <.D.) iff ( D c= b3 &amp; ( for F being Filter of L st D c= F holds
b3 c= F ) ) );

theorem Th21: :: FILTER_0:21
for L being Lattice
for F being Filter of L holds <.F.) = F
proofend;

theorem Th22: :: FILTER_0:22
for L being Lattice
for D1, D2 being non empty Subset of L st D1 c= D2 holds
<.D1.) c= <.D2.)
proofend;

theorem Th23: :: FILTER_0:23
for L being Lattice
for p being Element of L
for D being non empty Subset of L st p in D holds
<.p.) c= <.D.)
proofend;

theorem Th24: :: FILTER_0:24
for L being Lattice
for p being Element of L
for D being non empty Subset of L st D = {p} holds
<.D.) = <.p.)
proofend;

theorem Th25: :: FILTER_0:25
for L being Lattice
for D being non empty Subset of L st L is 0_Lattice &amp; Bottom L in D holds
( <.D.) = <.L.) &amp; <.D.) = the carrier of L )
proofend;

theorem Th26: :: FILTER_0:26
for L being Lattice
for F being Filter of L st L is 0_Lattice &amp; Bottom L in F holds
( F = <.L.) &amp; F = the carrier of L )
proofend;

definition
let L be Lattice;
let F be Filter of L;
attrF is prime  means :: FILTER_0:def 5
 for p, q being Element of L holds
( p "\/" q in F iff ( p in F or q in F ) );
end;

:: deftheorem  defines prime FILTER_0:def_5_:_
 for L being Lattice
for F being Filter of L holds
( F is prime iff for p, q being Element of L holds
( p "\/" q in F iff ( p in F or q in F ) ) );

theorem Th27: :: FILTER_0:27
for L being Lattice st L is B_Lattice holds
for p, q being Element of L holds
( p "/\" ((p `) "\/" q) [= q &amp; ( for r being Element of L st p "/\" r [= q holds
r [= (p `) "\/" q ) )
proofend;

definition
let IT be non empty LattStr ;
attrIT is implicative  means :Def6: :: FILTER_0:def 6
 for p, q being Element of IT ex r being Element of IT st
( p "/\" r [= q &amp; ( for r1 being Element of IT st p "/\" r1 [= q holds
r1 [= r ) );
end;

:: deftheorem Def6 defines implicative FILTER_0:def_6_:_
 for IT being non empty LattStr holds
( IT is implicative iff for p, q being Element of IT ex r being Element of IT st
( p "/\" r [= q &amp; ( for r1 being Element of IT st p "/\" r1 [= q holds
r1 [= r ) ) );

registration
cluster non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like implicative for LattStr ;
existence
 ex b1 being Lattice st
( b1 is strict &amp; b1 is implicative )
proofend;
end;

definition
mode I_Lattice is implicative Lattice;
end;

definition
let L be Lattice;
let p, q be Element of L;
assume A1: L is I_Lattice ;
funcp => q ->  Element of L means :Def7: :: FILTER_0:def 7
( p "/\" it [= q &amp; ( for r being Element of L st p "/\" r [= q holds
r [= it ) );
existence
 ex b1 being Element of L st
( p "/\" b1 [= q &amp; ( for r being Element of L st p "/\" r [= q holds
r [= b1 ) ) by A1, Def6;
correctness
uniqueness
for b1, b2 being Element of L st p "/\" b1 [= q &amp; ( for r being Element of L st p "/\" r [= q holds
r [= b1 ) &amp; p "/\" b2 [= q &amp; ( for r being Element of L st p "/\" r [= q holds
r [= b2 ) holds
b1 = b2;
proofend;
end;

:: deftheorem Def7 defines => FILTER_0:def_7_:_
 for L being Lattice
for p, q being Element of L st L is I_Lattice holds
for b4 being Element of L holds
( b4 = p => q iff ( p "/\" b4 [= q &amp; ( for r being Element of L st p "/\" r [= q holds
r [= b4 ) ) );

registration
cluster non empty Lattice-like implicative  ->  upper-bounded for LattStr ;
coherence
 for b1 being I_Lattice holds b1 is upper-bounded
proofend;
end;

theorem Th28: :: FILTER_0:28
for I being I_Lattice
for i being Element of I holds i => i = Top I
proofend;

registration
cluster non empty Lattice-like implicative  ->  distributive for LattStr ;
coherence
 for b1 being I_Lattice holds b1 is distributive
proofend;
end;

registration
cluster non empty Lattice-like Boolean  ->  implicative for LattStr ;
coherence
 for b1 being B_Lattice holds b1 is implicative
proofend;
end;

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

theorem Th29: :: FILTER_0:29
for I being I_Lattice
for i, j being Element of I
for FI being Filter of I st i in FI &amp; i => j in FI holds
j in FI
proofend;

theorem Th30: :: FILTER_0:30
for I being I_Lattice
for j, i being Element of I
for FI being Filter of I st j in FI holds
i => j in FI
proofend;

definition
let L be Lattice;
let D1, D2 be non empty Subset of L;
funcD1 "/\" D2 ->  Subset of L equals :: FILTER_0:def 8
 {  (p "/\" q) where p, q is Element of L : ( p in D1 &amp; q in D2 )  }  ;
coherence
  {  (p "/\" q) where p, q is Element of L : ( p in D1 &amp; q in D2 )  }  is Subset of L
proofend;
end;

:: deftheorem  defines "/\" FILTER_0:def_8_:_
 for L being Lattice
for D1, D2 being non empty Subset of L holds D1 "/\" D2 =  {  (p "/\" q) where p, q is Element of L : ( p in D1 &amp; q in D2 )  }  ;

registration
let L be Lattice;
let D1, D2 be non empty Subset of L;
clusterD1 "/\" D2 ->  non empty ;
coherence
 not D1 "/\" D2 is empty
proofend;
end;

theorem :: FILTER_0:31
for L being Lattice
for p, q being Element of L
for D1, D2 being non empty Subset of L st p in D1 &amp; q in D2 holds
( p "/\" q in D1 "/\" D2 &amp; q "/\" p in D1 "/\" D2 ) ;

theorem :: FILTER_0:32
for L being Lattice
for x being set
for D1, D2 being non empty Subset of L st x in D1 "/\" D2 holds
ex p, q being Element of L st
( x = p "/\" q &amp; p in D1 &amp; q in D2 ) ;

theorem Th33: :: FILTER_0:33
for L being Lattice
for D1, D2 being non empty Subset of L holds D1 "/\" D2 = D2 "/\" D1
proofend;

registration
let L be D_Lattice;
let F1, F2 be Filter of L;
clusterF1 "/\" F2 ->  final meet-closed ;
coherence
 ( F1 "/\" F2 is final &amp; F1 "/\" F2 is meet-closed )
proofend;
end;

theorem Th34: :: FILTER_0:34
for L being Lattice
for D1, D2 being non empty Subset of L holds
( <.(D1 \/ D2).) = <.(<.D1.) \/ D2).) &amp; <.(D1 \/ D2).) = <.(D1 \/ <.D2.)).) )
proofend;

theorem :: FILTER_0:35
for L being Lattice
for F, H being Filter of L holds <.(F \/ H).) =  {  r where r is Element of L : ex p, q being Element of L st
( p "/\" q [= r &amp; p in F &amp; q in H )  }
proofend;

theorem Th36: :: FILTER_0:36
for L being Lattice
for F, H being Filter of L holds
( F c= F "/\" H &amp; H c= F "/\" H )
proofend;

theorem Th37: :: FILTER_0:37
for L being Lattice
for F, H being Filter of L holds <.(F \/ H).) = <.(F "/\" H).)
proofend;

theorem Th38: :: FILTER_0:38
for I being I_Lattice
for F1, F2 being Filter of I holds <.(F1 \/ F2).) = F1 "/\" F2
proofend;

theorem :: FILTER_0:39
for B being B_Lattice
for FB, HB being Filter of B holds <.(FB \/ HB).) = FB "/\" HB
proofend;

theorem Th40: :: FILTER_0:40
for I being I_Lattice
for j, i being Element of I
for DI being non empty Subset of I st j in <.(DI \/ {i}).) holds
i => j in <.DI.)
proofend;

theorem Th41: :: FILTER_0:41
for I being I_Lattice
for i, j, k being Element of I
for FI being Filter of I st i => j in FI &amp; j => k in FI holds
i => k in FI
proofend;

theorem Th42: :: FILTER_0:42
for B being B_Lattice
for a, b being Element of B holds a => b = (a `) "\/" b
proofend;

theorem Th43: :: FILTER_0:43
for B being B_Lattice
for a, b being Element of B holds
( a [= b iff a "/\" (b `) = Bottom B )
proofend;

theorem Th44: :: FILTER_0:44
for B being B_Lattice
for FB being Filter of B holds
( FB is being_ultrafilter iff ( FB <> the carrier of B &amp; ( for a being Element of B holds
( a in FB or a ` in FB ) ) ) )
proofend;

theorem :: FILTER_0:45
for B being B_Lattice
for FB being Filter of B holds
( ( FB <> <.B.) &amp; FB is prime ) iff FB is being_ultrafilter )
proofend;

theorem Th46: :: FILTER_0:46
for B being B_Lattice
for FB being Filter of B st FB is being_ultrafilter holds
for a being Element of B holds
( a in FB iff not a ` in FB )
proofend;

theorem :: FILTER_0:47
for B being B_Lattice
for a, b being Element of B st a <> b holds
ex FB being Filter of B st
( FB is being_ultrafilter &amp; ( ( a in FB &amp; not b in FB ) or ( not a in FB &amp; b in FB ) ) )
proofend;

definition
let L be Lattice;
let F be Filter of L;
func latt F ->  Lattice means :Def9: :: FILTER_0:def 9
 ex o1, o2 being BinOp of F st
( o1 = the L_join of L || F &amp; o2 = the L_meet of L || F &amp; it = LattStr(# F,o1,o2 #) );
uniqueness
 for b1, b2 being Lattice st ex o1, o2 being BinOp of F st
( o1 = the L_join of L || F &amp; o2 = the L_meet of L || F &amp; b1 = LattStr(# F,o1,o2 #) ) &amp; ex o1, o2 being BinOp of F st
( o1 = the L_join of L || F &amp; o2 = the L_meet of L || F &amp; b2 = LattStr(# F,o1,o2 #) ) holds
b1 = b2 ;
existence
 ex b1 being Lattice ex o1, o2 being BinOp of F st
( o1 = the L_join of L || F &amp; o2 = the L_meet of L || F &amp; b1 = LattStr(# F,o1,o2 #) )
proofend;
end;

:: deftheorem Def9 defines latt FILTER_0:def_9_:_
 for L being Lattice
for F being Filter of L
for b3 being Lattice holds
( b3 = latt F iff ex o1, o2 being BinOp of F st
( o1 = the L_join of L || F &amp; o2 = the L_meet of L || F &amp; b3 = LattStr(# F,o1,o2 #) ) );

registration
let L be Lattice;
let F be Filter of L;
cluster latt F ->  strict ;
coherence
 latt F is strict
proofend;
end;

theorem :: FILTER_0:48
for L being strict Lattice holds latt <.L.) = L
proofend;

theorem Th49: :: FILTER_0:49
for L being Lattice
for F being Filter of L holds
( the carrier of (latt F) = F &amp; the L_join of (latt F) = the L_join of L || F &amp; the L_meet of (latt F) = the L_meet of L || F )
proofend;

theorem Th50: :: FILTER_0:50
for L being Lattice
for p, q being Element of L
for F being Filter of L
for p9, q9 being Element of (latt F) st p = p9 &amp; q = q9 holds
( p "\/" q = p9 "\/" q9 &amp; p "/\" q = p9 "/\" q9 )
proofend;

theorem Th51: :: FILTER_0:51
for L being Lattice
for p, q being Element of L
for F being Filter of L
for p9, q9 being Element of (latt F) st p = p9 &amp; q = q9 holds
( p [= q iff p9 [= q9 )
proofend;

theorem Th52: :: FILTER_0:52
for L being Lattice
for F being Filter of L st L is upper-bounded holds
latt F is upper-bounded
proofend;

theorem :: FILTER_0:53
for L being Lattice
for F being Filter of L st L is modular holds
latt F is modular
proofend;

theorem Th54: :: FILTER_0:54
for L being Lattice
for F being Filter of L st L is distributive holds
latt F is distributive
proofend;

theorem :: FILTER_0:55
for L being Lattice
for F being Filter of L st L is I_Lattice holds
latt F is implicative
proofend;

registration
let L be Lattice;
let p be Element of L;
cluster latt <.p.) ->  lower-bounded ;
coherence
 latt <.p.) is lower-bounded
proofend;
end;

theorem Th56: :: FILTER_0:56
for L being Lattice
for p being Element of L holds Bottom (latt <.p.)) = p
proofend;

theorem Th57: :: FILTER_0:57
for L being Lattice
for p being Element of L st L is upper-bounded holds
Top (latt <.p.)) = Top L
proofend;

theorem Th58: :: FILTER_0:58
for L being Lattice
for p being Element of L st L is 1_Lattice holds
latt <.p.) is bounded
proofend;

theorem Th59: :: FILTER_0:59
for L being Lattice
for p being Element of L st L is C_Lattice &amp; L is M_Lattice holds
latt <.p.) is C_Lattice
proofend;

theorem :: FILTER_0:60
for L being Lattice
for p being Element of L st L is B_Lattice holds
latt <.p.) is B_Lattice
proofend;

definition
let L be Lattice;
let p, q be Element of L;
funcp <=> q ->  Element of L equals :: FILTER_0:def 10
(p => q) "/\" (q => p);
correctness
coherence
(p => q) "/\" (q => p) is Element of L;
;
end;

:: deftheorem  defines <=> FILTER_0:def_10_:_
 for L being Lattice
for p, q being Element of L holds p <=> q = (p => q) "/\" (q => p);

theorem :: FILTER_0:61
for L being Lattice
for p, q being Element of L holds p <=> q = q <=> p ;

theorem Th62: :: FILTER_0:62
for I being I_Lattice
for i, j, k being Element of I
for FI being Filter of I st i <=> j in FI &amp; j <=> k in FI holds
i <=> k in FI
proofend;

definition
let L be Lattice;
let F be Filter of L;
func equivalence_wrt F ->  Relation means :Def11: :: FILTER_0:def 11
( field it c= the carrier of L &amp; ( for p, q being Element of L holds
( [p,q] in it iff p <=> q in F ) ) );
existence
 ex b1 being Relation st
( field b1 c= the carrier of L &amp; ( for p, q being Element of L holds
( [p,q] in b1 iff p <=> q in F ) ) )
proofend;
uniqueness
 for b1, b2 being Relation st field b1 c= the carrier of L &amp; ( for p, q being Element of L holds
( [p,q] in b1 iff p <=> q in F ) ) &amp; field b2 c= the carrier of L &amp; ( for p, q being Element of L holds
( [p,q] in b2 iff p <=> q in F ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def11 defines equivalence_wrt FILTER_0:def_11_:_
 for L being Lattice
for F being Filter of L
for b3 being Relation holds
( b3 = equivalence_wrt F iff ( field b3 c= the carrier of L &amp; ( for p, q being Element of L holds
( [p,q] in b3 iff p <=> q in F ) ) ) );

theorem Th63: :: FILTER_0:63
for L being Lattice
for F being Filter of L holds equivalence_wrt F is Relation of the carrier of L
proofend;

theorem Th64: :: FILTER_0:64
for L being Lattice
for F being Filter of L st L is I_Lattice holds
equivalence_wrt F is_reflexive_in the carrier of L
proofend;

theorem Th65: :: FILTER_0:65
for L being Lattice
for F being Filter of L holds equivalence_wrt F is_symmetric_in the carrier of L
proofend;

theorem Th66: :: FILTER_0:66
for L being Lattice
for F being Filter of L st L is I_Lattice holds
equivalence_wrt F is_transitive_in the carrier of L
proofend;

theorem Th67: :: FILTER_0:67
for L being Lattice
for F being Filter of L st L is I_Lattice holds
equivalence_wrt F is Equivalence_Relation of the carrier of L
proofend;

theorem :: FILTER_0:68
for L being Lattice
for F being Filter of L st L is I_Lattice holds
field (equivalence_wrt F) = the carrier of L
proofend;

definition
let I be I_Lattice;
let FI be Filter of I;
:: original:equivalence_wrt
redefine func equivalence_wrt FI ->  Equivalence_Relation of the carrier of I;
coherence
 equivalence_wrt FI is Equivalence_Relation of the carrier of I by Th67;
end;

definition
let B be B_Lattice;
let FB be Filter of B;
:: original:equivalence_wrt
redefine func equivalence_wrt FB ->  Equivalence_Relation of the carrier of B;
coherence
 equivalence_wrt FB is Equivalence_Relation of the carrier of B by Th67;
end;

definition
let L be Lattice;
let F be Filter of L;
let p, q be Element of L;
predp,q are_equivalence_wrt F means :Def12: :: FILTER_0:def 12
p <=> q in F;
end;

:: deftheorem Def12 defines are_equivalence_wrt FILTER_0:def_12_:_
 for L being Lattice
for F being Filter of L
for p, q being Element of L holds
( p,q are_equivalence_wrt F iff p <=> q in F );

theorem :: FILTER_0:69
for L being Lattice
for p, q being Element of L
for F being Filter of L holds
( p,q are_equivalence_wrt F iff [p,q] in equivalence_wrt F )
proofend;

theorem :: FILTER_0:70
for B being B_Lattice
for FB being Filter of B
for I being I_Lattice
for i being Element of I
for FI being Filter of I
for a being Element of B holds
( i,i are_equivalence_wrt FI &amp; a,a are_equivalence_wrt FB )
proofend;

theorem :: FILTER_0:71
for L being Lattice
for p, q being Element of L
for F being Filter of L st p,q are_equivalence_wrt F holds
q,p are_equivalence_wrt F
proofend;

theorem :: FILTER_0:72
for B being B_Lattice
for FB being Filter of B
for I being I_Lattice
for i, j, k being Element of I
for FI being Filter of I
for a, b, c being Element of B holds
( ( i,j are_equivalence_wrt FI &amp; j,k are_equivalence_wrt FI implies i,k are_equivalence_wrt FI ) &amp; ( a,b are_equivalence_wrt FB &amp; b,c are_equivalence_wrt FB implies a,c are_equivalence_wrt FB ) )
proofend;

begin

:: missing, 2006.12.05, AT
theorem :: FILTER_0:73
for L being non empty join-commutative meet-commutative meet-associative meet-absorbing join-absorbing LattStr
for x, y, z being Element of L st z [= x &amp; z [= y &amp; ( for z9 being Element of L st z9 [= x &amp; z9 [= y holds
z9 [= z ) holds
z = x "/\" y
proofend;

theorem :: FILTER_0:74
for L being non empty join-commutative join-associative meet-commutative meet-absorbing join-absorbing LattStr
for x, y, z being Element of L st x [= z &amp; y [= z &amp; ( for z9 being Element of L st x [= z9 &amp; y [= z9 holds
z [= z9 ) holds
z = x "\/" y
proofend;