:: FILTER_0 semantic presentation

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
proof
let L be non empty join-commutative join-associative meet-commutative meet-absorbing join-absorbing LattStr ; ::_thesis: for p, q, r being Element of L st p [= q holds
r "\/" p [= r "\/" q
let p, q, r be Element of L; ::_thesis: ( p [= q implies r "\/" p [= r "\/" q )
assume A1: p "\/" q = q ; :: according to LATTICES:def_3 ::_thesis: r "\/" p [= r "\/" q
thus (r "\/" p) "\/" (r "\/" q) = (r "\/" (r "\/" p)) "\/" q by LATTICES:def_5
.= ((r "\/" r) "\/" p) "\/" q by LATTICES:def_5
.= (r "\/" p) "\/" q
.= r "\/" q by A1, LATTICES:def_5 ; :: according to LATTICES:def_3 ::_thesis: verum
end;

theorem :: FILTER_0:2
for L being Lattice
for p, r, q being Element of L st p [= r holds
p "/\" q [= r
proof
let L be Lattice; ::_thesis: for p, r, q being Element of L st p [= r holds
p "/\" q [= r
let p, r, q be Element of L; ::_thesis: ( p [= r implies p "/\" q [= r )
assume  p [= r ; ::_thesis: p "/\" q [= r
then A1: p "/\" q [= r "/\" q by LATTICES:9;
 r "/\" q [= r by LATTICES:6;
hence  p "/\" q [= r by A1, LATTICES:7; ::_thesis: verum
end;

theorem :: FILTER_0:3
for L being Lattice
for p, r, q being Element of L st p [= r holds
p [= q "\/" r
proof
let L be Lattice; ::_thesis: for p, r, q being Element of L st p [= r holds
p [= q "\/" r
let p, r, q be Element of L; ::_thesis: ( p [= r implies p [= q "\/" r )
assume  p [= r ; ::_thesis: p [= q "\/" r
then A1: p "\/" q [= r "\/" q by Th1;
 p [= p "\/" q by LATTICES:5;
hence  p [= q "\/" r by A1, LATTICES:7; ::_thesis: verum
end;

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
proof
let L be non empty join-commutative join-associative join-absorbing LattStr ; ::_thesis: for a, b, c, d being Element of L st a [= b & c [= d holds
a "\/" c [= b "\/" d
let a, b, c, d be Element of L; ::_thesis: ( a [= b & c [= d implies a "\/" c [= b "\/" d )
assume  a [= b ; ::_thesis: ( not c [= d or a "\/" c [= b "\/" d )
then A1: b = a "\/" b by LATTICES:def_3;
assume  c [= d ; ::_thesis: a "\/" c [= b "\/" d
then b "\/" d = (a "\/" b) "\/" (c "\/" d) by A1, LATTICES:def_3
.= ((b "\/" a) "\/" c) "\/" d by LATTICES:def_5
.= (b "\/" (a "\/" c)) "\/" d by LATTICES:def_5
.= (a "\/" c) "\/" (b "\/" d) by LATTICES:def_5 ;
hence  a "\/" c [= b "\/" d by LATTICES:def_3; ::_thesis: verum
end;

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
proof
let L be non empty meet-commutative meet-associative meet-absorbing join-absorbing LattStr ; ::_thesis: for a, b, c, d being Element of L st a [= b & c [= d holds
a "/\" c [= b "/\" d
let a, b, c, d be Element of L; ::_thesis: ( a [= b & c [= d implies a "/\" c [= b "/\" d )
assume  a [= b ; ::_thesis: ( not c [= d or a "/\" c [= b "/\" d )
then A1: a "/\" b = a by LATTICES:4;
assume  c [= d ; ::_thesis: a "/\" c [= b "/\" d
then a "/\" c = (a "/\" b) "/\" (c "/\" d) by A1, LATTICES:4
.= ((a "/\" b) "/\" c) "/\" d by LATTICES:def_7
.= (b "/\" (a "/\" c)) "/\" d by LATTICES:def_7
.= (a "/\" c) "/\" (b "/\" d) by LATTICES:def_7 ;
hence  a "/\" c [= b "/\" d by LATTICES:4; ::_thesis: verum
end;

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
proof
let L be non empty join-commutative join-associative meet-commutative meet-absorbing join-absorbing LattStr ; ::_thesis: for a, b, c being Element of L st a [= c & b [= c holds
a "\/" b [= c
let a, b, c be Element of L; ::_thesis: ( a [= c & b [= c implies a "\/" b [= c )
 c "\/" c = c ;
hence  ( a [= c & b [= c implies a "\/" b [= c ) by Th4; ::_thesis: verum
end;

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
proof
let L be non empty meet-commutative meet-associative meet-absorbing join-absorbing LattStr ; ::_thesis: for a, b, c being Element of L st a [= b & a [= c holds
a [= b "/\" c
let a, b, c be Element of L; ::_thesis: ( a [= b & a [= c implies a [= b "/\" c )
 a "/\" a = a ;
hence  ( a [= b & a [= c implies a [= b "/\" c ) by Th5; ::_thesis: verum
end;

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 ) )
proof
let L be Lattice; ::_thesis: 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 ) )
let S be non empty Subset of L; ::_thesis: ( 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 ) )
thus  ( S is Filter of L implies for p, q being Element of L holds
( ( p in S & q in S ) iff p "/\" q in S ) ) ::_thesis: ( ( for p, q being Element of L holds
( ( p in S & q in S ) iff p "/\" q in S ) ) implies S is Filter of L )
proof
assume A1: S is Filter of L ; ::_thesis: for p, q being Element of L holds
( ( p in S & q in S ) iff p "/\" q in S )
let p, q be Element of L; ::_thesis: ( ( p in S & q in S ) iff p "/\" q in S )
thus  ( p in S & q in S implies p "/\" q in S ) by A1, LATTICES:def_24; ::_thesis: ( p "/\" q in S implies ( p in S & q in S ) )
assume A2: p "/\" q in S ; ::_thesis: ( p in S & q in S )
 ( p "/\" q [= p & p "/\" q [= q ) by LATTICES:6;
hence  ( p in S & q in S ) by A1, A2, LATTICES:def_23; ::_thesis: verum
end;
assume A3: for p, q being Element of L holds
( ( p in S & q in S ) iff p "/\" q in S ) ; ::_thesis: S is Filter of L
 S is final
proof
let p, q be Element of L; :: according to LATTICES:def_23 ::_thesis: ( not p [= q or not p in S or q in S )
assume that
A4: p [= q and
A5: p in S ; ::_thesis: q in S
 p "/\" q = p by A4, LATTICES:4;
hence  q in S by A3, A5; ::_thesis: verum
end;
hence  S is Filter of L by A3, LATTICES:def_24; ::_thesis: verum
end;

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 ) ) )
proof
let L be Lattice; ::_thesis: 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 ) ) )
let D be non empty Subset of L; ::_thesis: ( 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 ) ) )
thus  ( D is Filter of L implies ( ( 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 ) ) ) by LATTICES:def_23, LATTICES:def_24; ::_thesis: ( ( 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 ) implies D is Filter of L )
assume A1: ( ( 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 ) ) ; ::_thesis: D is Filter of L
then  for p, q being Element of L st p [= q & p in D holds
q in D ;
hence  D is Filter of L by A1, LATTICES:def_23, LATTICES:def_24; ::_thesis: verum
end;


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 )
proof
let L be Lattice; ::_thesis: 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 )
let p, q be Element of L; ::_thesis: for H being Filter of L st p in H holds
( p "\/" q in H & q "\/" p in H )
let H be Filter of L; ::_thesis: ( p in H implies ( p "\/" q in H & q "\/" p in H ) )
 p [= p "\/" q by LATTICES:5;
hence  ( p in H implies ( p "\/" q in H & q "\/" p in H ) ) by Th9; ::_thesis: verum
end;

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
proof
let L be Lattice; ::_thesis: for H being Filter of L st L is 1_Lattice holds
Top L in H
let H be Filter of L; ::_thesis: ( L is 1_Lattice implies Top L in H )
assume  L is 1_Lattice ; ::_thesis: Top L in H
then reconsider L = L as 1_Lattice ;
consider p being Element of L such that
A1: p in H by SUBSET_1:4;
 p [= Top L by LATTICES:19;
hence  Top L in H by A1, Th9; ::_thesis: verum
end;

theorem :: FILTER_0:12
for L being Lattice st L is 1_Lattice holds
{(Top L)} is Filter of L
proof
let L be Lattice; ::_thesis: ( L is 1_Lattice implies {(Top L)} is Filter of L )
assume  L is 1_Lattice ; ::_thesis: {(Top L)} is Filter of L
then reconsider K = L as 1_Lattice ;
now__::_thesis:_for_p,_q_being_Element_of_K_holds_
(_(_p_in_{(Top_K)}_&_q_in_{(Top_K)}_implies_p_"/\"_q_in_{(Top_K)}_)_&_(_p_"/\"_q_in_{(Top_K)}_implies_(_p_in_{(Top_K)}_&_q_in_{(Top_K)}_)_)_)
let p, q be Element of K; ::_thesis: ( ( p in {(Top K)} & q in {(Top K)} implies p "/\" q in {(Top K)} ) & ( p "/\" q in {(Top K)} implies ( p in {(Top K)} & q in {(Top K)} ) ) )
A1: ( p [= Top K & q [= Top K ) by LATTICES:19;
A2: ( p in {(Top K)} iff p = Top K ) by TARSKI:def_1;
hence  ( p in {(Top K)} & q in {(Top K)} implies p "/\" q in {(Top K)} ) by LATTICES:17; ::_thesis: ( p "/\" q in {(Top K)} implies ( p in {(Top K)} & q in {(Top K)} ) )
assume  p "/\" q in {(Top K)} ; ::_thesis: ( p in {(Top K)} & q in {(Top K)} )
then A3: p "/\" q = Top K by TARSKI:def_1;
 ( p "/\" q [= p & q "/\" p [= q ) by LATTICES:6;
hence  ( p in {(Top K)} & q in {(Top K)} ) by A2, A3, A1, LATTICES:8; ::_thesis: verum
end;
hence  {(Top L)} is Filter of L by Th8; ::_thesis: verum
end;

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
proof
let L be Lattice; ::_thesis: for p being Element of L st {p} is Filter of L holds
L is upper-bounded
let p be Element of L; ::_thesis: ( {p} is Filter of L implies L is upper-bounded )
assume  {p} is Filter of L ; ::_thesis: L is upper-bounded
then reconsider F = {p} as Filter of L ;
take  p ; :: according to LATTICES:def_14 ::_thesis: for b1 being Element of the carrier of L holds
( p "\/" b1 = p & b1 "\/" p = p )
let q be Element of L; ::_thesis: ( p "\/" q = p & q "\/" p = p )
 p in F by TARSKI:def_1;
then  p "\/" q in F by Th10;
hence  ( p "\/" q = p & q "\/" p = p ) by TARSKI:def_1; ::_thesis: verum
end;

theorem Th14: :: FILTER_0:14
for L being Lattice holds the carrier of L is Filter of L
proof
let L be Lattice; ::_thesis: the carrier of L is Filter of L
 the carrier of L = [#] L ;
hence  the carrier of L is Filter of L ; ::_thesis: verum
end;

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
proof
set D =  {  q where q is Element of L : p [= q  }  ;
 p in  {  q where q is Element of L : p [= q  }  ;
then reconsider F =  {  q where q is Element of L : p [= q  }  as non empty set ;
 F c= the carrier of L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F or x in the carrier of L )
assume  x in F ; ::_thesis: x in the carrier of L
then  ex q being Element of L st
( x = q & p [= q ) ;
hence  x in the carrier of L ; ::_thesis: verum
end;
then reconsider F = F as non empty Subset of L ;
A1: now__::_thesis:_for_r,_q_being_Element_of_L_st_r_in_F_&_q_in_F_holds_
r_"/\"_q_in_F
let r, q be Element of L; ::_thesis: ( r in F & q in F implies r "/\" q in F )
assume  r in F ; ::_thesis: ( q in F implies r "/\" q in F )
then  ex r1 being Element of L st
( r = r1 & p [= r1 ) ;
then A2: p "/\" p [= r "/\" p by LATTICES:9;
assume  q in F ; ::_thesis: r "/\" q in F
then  ex q1 being Element of L st
( q = q1 & p [= q1 ) ;
then A3: p "/\" r [= q "/\" r by LATTICES:9;
 p [= r "/\" q by A3, A2, LATTICES:7;
hence  r "/\" q in F ; ::_thesis: verum
end;
now__::_thesis:_for_r,_q_being_Element_of_L_st_r_in_F_&_r_[=_q_holds_
q_in_F
let r, q be Element of L; ::_thesis: ( r in F & r [= q implies q in F )
assume  r in F ; ::_thesis: ( r [= q implies q in F )
then A4: ex r1 being Element of L st
( r = r1 & p [= r1 ) ;
assume  r [= q ; ::_thesis: q in F
then  p [= q by A4, LATTICES:7;
hence  q in F ; ::_thesis: verum
end;
hence   {  q where q is Element of L : p [= q  }  is Filter of L by A1, Th9; ::_thesis: verum
end;
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 )
proof
let L be Lattice; ::_thesis: for q, p being Element of L holds
( q in <.p.) iff p [= q )
let q, p be Element of L; ::_thesis: ( q in <.p.) iff p [= q )
 ( q in <.p.) iff ex r being Element of L st
( q = r & p [= r ) ) ;
hence  ( q in <.p.) iff p [= q ) ; ::_thesis: verum
end;

theorem Th16: :: FILTER_0:16
for L being Lattice
for p, q being Element of L holds
( p in <.p.) & p "\/" q in <.p.) & q "\/" p in <.p.) )
proof
let L be Lattice; ::_thesis: for p, q being Element of L holds
( p in <.p.) & p "\/" q in <.p.) & q "\/" p in <.p.) )
let p, q be Element of L; ::_thesis: ( p in <.p.) & p "\/" q in <.p.) & q "\/" p in <.p.) )
 p [= p "\/" q by LATTICES:5;
hence  ( p in <.p.) & p "\/" q in <.p.) & q "\/" p in <.p.) ) ; ::_thesis: verum
end;

theorem Th17: :: FILTER_0:17
for L being Lattice st L is 0_Lattice holds
<.L.) = <.(Bottom L).)
proof
let L be Lattice; ::_thesis: ( L is 0_Lattice implies <.L.) = <.(Bottom L).) )
assume  L is 0_Lattice ; ::_thesis: <.L.) = <.(Bottom L).)
then reconsider L9 = L as 0_Lattice ;
thus  <.L.) c= <.(Bottom L).) :: according to XBOOLE_0:def_10 ::_thesis: <.(Bottom L).) c= <.L.)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in <.L.) or x in <.(Bottom L).) )
assume  x in <.L.) ; ::_thesis: x in <.(Bottom L).)
then reconsider x = x as Element of L9 ;
 ( Bottom L in <.(Bottom L).) & x "/\" (Bottom L9) = Bottom L9 ) ;
hence  x in <.(Bottom L).) by Th8; ::_thesis: verum
end;
thus  <.(Bottom L).) c= <.L.) ; ::_thesis: verum
end;

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 & ( for H being Filter of L st F c= H & 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 & ( for H being Filter of L st F c= H & 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 & H is being_ultrafilter )
proof
let L be Lattice; ::_thesis: ( L is lower-bounded implies for F being Filter of L st F <> the carrier of L holds
ex H being Filter of L st
( F c= H & H is being_ultrafilter ) )
given r being Element of L such that A1: for p being Element of L holds
( r "/\" p = r & p "/\" r = r ) ; :: according to LATTICES:def_13 ::_thesis: for F being Filter of L st F <> the carrier of L holds
ex H being Filter of L st
( F c= H & H is being_ultrafilter )
A2: for H being Filter of L st r in H holds
H = the carrier of L
proof
let H be Filter of L; ::_thesis: ( r in H implies H = the carrier of L )
assume A3: r in H ; ::_thesis: H = the carrier of L
thus  H c= the carrier of L ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of L c= H
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of L or x in H )
assume  x in the carrier of L ; ::_thesis: x in H
then reconsider p = x as Element of L ;
 r "/\" p = r by A1;
then  r [= p by LATTICES:4;
hence  x in H by A3, Th9; ::_thesis: verum
end;
let F be Filter of L; ::_thesis: ( F <> the carrier of L implies ex H being Filter of L st
( F c= H & H is being_ultrafilter ) )
assume A4: F <> the carrier of L ; ::_thesis: ex H being Filter of L st
( F c= H & H is being_ultrafilter )
set X =  {  A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L )  }  ;
A5: for x being set st x in  {  A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L )  }  holds
( x is Subset of L & x is Filter of L )
proof
let x be set ; ::_thesis: ( x in  {  A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L )  }  implies ( x is Subset of L & x is Filter of L ) )
assume  x in  {  A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L )  }  ; ::_thesis: ( x is Subset of L & x is Filter of L )
then  ex A being Subset of L st
( x = A & F c= A & A is Filter of L & A <> the carrier of L ) ;
hence  ( x is Subset of L & x is Filter of L ) ; ::_thesis: verum
end;
A6: for X1 being set st X1 in  {  A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L )  }  holds
( F,X1 are_c=-comparable & X1 <> the carrier of L )
proof
let X1 be set ; ::_thesis: ( X1 in  {  A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L )  }  implies ( F,X1 are_c=-comparable & X1 <> the carrier of L ) )
assume  X1 in  {  A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L )  }  ; ::_thesis: ( F,X1 are_c=-comparable & X1 <> the carrier of L )
then  ex A being Subset of L st
( X1 = A & F c= A & A is Filter of L & A <> the carrier of L ) ;
hence  ( F,X1 are_c=-comparable & X1 <> the carrier of L ) by XBOOLE_0:def_9; ::_thesis: verum
end;
A7: for Z being set st Z c=  {  A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L )  }  & Z is c=-linear holds
ex Y being set st
( Y in  {  A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L )  }  & ( for X1 being set st X1 in Z holds
X1 c= Y ) )
proof
set x = the Element of F;
let Z be set ; ::_thesis: ( Z c=  {  A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L )  }  & Z is c=-linear implies ex Y being set st
( Y in  {  A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L )  }  & ( for X1 being set st X1 in Z holds
X1 c= Y ) ) )
assume that
A8: Z c=  {  A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L )  }  and
A9: Z is c=-linear ; ::_thesis: ex Y being set st
( Y in  {  A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L )  }  & ( for X1 being set st X1 in Z holds
X1 c= Y ) )
take Y = union (Z \/ {F}); ::_thesis: ( Y in  {  A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L )  }  & ( for X1 being set st X1 in Z holds
X1 c= Y ) )
 F in {F} by TARSKI:def_1;
then A10: F in Z \/ {F} by XBOOLE_0:def_3;
 the Element of F in F ;
then reconsider V = Y as non empty set by A10, TARSKI:def_4;
 V c= the carrier of L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in V or x in the carrier of L )
assume  x in V ; ::_thesis: x in the carrier of L
then consider X1 being set  such that
A11: x in X1 and
A12: X1 in Z \/ {F} by TARSKI:def_4;
 ( X1 in Z or X1 in {F} ) by A12, XBOOLE_0:def_3;
then  X1 is Subset of L by A5, A8;
hence  x in the carrier of L by A11; ::_thesis: verum
end;
then reconsider V = V as non empty Subset of L ;
now__::_thesis:_for_p,_q_being_Element_of_L_holds_
(_(_p_in_V_&_q_in_V_implies_p_"/\"_q_in_V_)_&_(_p_"/\"_q_in_V_implies_(_p_in_V_&_q_in_V_)_)_)
let p, q be Element of L; ::_thesis: ( ( p in V & q in V implies p "/\" q in V ) & ( p "/\" q in V implies ( p in V & q in V ) ) )
thus  ( p in V & q in V implies p "/\" q in V ) ::_thesis: ( p "/\" q in V implies ( p in V & q in V ) )
proof
assume  p in V ; ::_thesis: ( not q in V or p "/\" q in V )
then consider X1 being set  such that
A13: p in X1 and
A14: X1 in Z \/ {F} by TARSKI:def_4;
A15: ( X1 in Z or X1 in {F} ) by A14, XBOOLE_0:def_3;
then A16: ( ( X1 in  {  A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L )  }  & X1 in Z ) or X1 = F ) by A8, TARSKI:def_1;
assume  q in V ; ::_thesis: p "/\" q in V
then consider X2 being set  such that
A17: q in X2 and
A18: X2 in Z \/ {F} by TARSKI:def_4;
A19: ( X2 in Z or X2 in {F} ) by A18, XBOOLE_0:def_3;
then  ( ( X2 in  {  A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L )  }  & X2 in Z ) or X2 = F ) by A8, TARSKI:def_1;
then  X1,X2 are_c=-comparable by A6, A9, A16, ORDINAL1:def_8;
then A20: ( X1 c= X2 or X2 c= X1 ) by XBOOLE_0:def_9;
A21: X1 is Filter of L by A5, A8, A15, TARSKI:def_1;
 X2 is Filter of L by A5, A8, A19, TARSKI:def_1;
then  ( p "/\" q in X1 or p "/\" q in X2 ) by A13, A17, A20, A21, Th9;
hence  p "/\" q in V by A14, A18, TARSKI:def_4; ::_thesis: verum
end;
assume  p "/\" q in V ; ::_thesis: ( p in V & q in V )
then consider X1 being set  such that
A22: p "/\" q in X1 and
A23: X1 in Z \/ {F} by TARSKI:def_4;
 ( X1 in Z or X1 in {F} ) by A23, XBOOLE_0:def_3;
then  X1 is Filter of L by A5, A8, TARSKI:def_1;
then  ( p in X1 & q in X1 ) by A22, Th8;
hence  ( p in V & q in V ) by A23, TARSKI:def_4; ::_thesis: verum
end;
then reconsider V = V as Filter of L by Th8;
now__::_thesis:_not_r_in_V
assume  r in V ; ::_thesis: contradiction
then consider X1 being set  such that
A24: r in X1 and
A25: X1 in Z \/ {F} by TARSKI:def_4;
 ( X1 in Z or X1 in {F} ) by A25, XBOOLE_0:def_3;
then  ( X1 in  {  A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L )  }  or X1 = F ) by A8, TARSKI:def_1;
then  ex A being Subset of L st
( X1 = A & F c= A & A is Filter of L & A <> the carrier of L ) by A4;
hence  contradiction by A2, A24; ::_thesis: verum
end;
then A26: V <> the carrier of L ;
 F c= V
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F or x in V )
thus  ( not x in F or x in V ) by A10, TARSKI:def_4; ::_thesis: verum
end;
hence  Y in  {  A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L )  }  by A26; ::_thesis: for X1 being set st X1 in Z holds
X1 c= Y
let X1 be set ; ::_thesis: ( X1 in Z implies X1 c= Y )
assume  X1 in Z ; ::_thesis: X1 c= Y
then  X1 in Z \/ {F} by XBOOLE_0:def_3;
hence  X1 c= Y by ZFMISC_1:74; ::_thesis: verum
end;
 F in  {  A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L )  }  by A4;
then consider Y being set  such that
A27: Y in  {  A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L )  }  and
A28: for Z being set st Z in  {  A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L )  }  & Z <> Y holds
not Y c= Z by A7, ORDERS_1:65;
consider H being Subset of L such that
A29: Y = H and
A30: F c= H and
A31: H is Filter of L and
A32: H <> the carrier of L by A27;
reconsider H = H as Filter of L by A31;
take  H ; ::_thesis: ( F c= H & H is being_ultrafilter )
thus  ( F c= H & H <> the carrier of L ) by A30, A32; :: according to FILTER_0:def_3 ::_thesis: for H being Filter of L st H c= H & H <> the carrier of L holds
H = H
let G be Filter of L; ::_thesis: ( H c= G & G <> the carrier of L implies H = G )
assume that
A33: H c= G and
A34: G <> the carrier of L ; ::_thesis: H = G
 F c= G by A30, A33, XBOOLE_1:1;
then  G in  {  A where A is Subset of L : ( F c= A & A is Filter of L & A <> the carrier of L )  }  by A34;
hence  H = G by A28, A29, A33; ::_thesis: verum
end;

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
proof
let L be Lattice; ::_thesis: for p being Element of L st ex r being Element of L st p "/\" r <> p holds
<.p.) <> the carrier of L
let p be Element of L; ::_thesis: ( ex r being Element of L st p "/\" r <> p implies <.p.) <> the carrier of L )
given r being Element of L such that A1: p "/\" r <> p ; ::_thesis: <.p.) <> the carrier of L
 p "/\" r [= p by LATTICES:6;
then  not p [= p "/\" r by A1, LATTICES:8;
hence  <.p.) <> the carrier of L by Th15; ::_thesis: verum
end;

theorem Th20: :: FILTER_0:20
for L being Lattice
for p being Element of L st L is 0_Lattice & p <> Bottom L holds
ex H being Filter of L st
( p in H & H is being_ultrafilter )
proof
let L be Lattice; ::_thesis: for p being Element of L st L is 0_Lattice & p <> Bottom L holds
ex H being Filter of L st
( p in H & H is being_ultrafilter )
let p be Element of L; ::_thesis: ( L is 0_Lattice & p <> Bottom L implies ex H being Filter of L st
( p in H & H is being_ultrafilter ) )
assume that
A1: L is 0_Lattice and
A2: p <> Bottom L ; ::_thesis: ex H being Filter of L st
( p in H & H is being_ultrafilter )
reconsider L9 = L as 0_Lattice by A1;
reconsider p9 = p as Element of L9 ;
 p9 "/\" (Bottom L9) = Bottom L9 ;
then consider H being Filter of L such that
A3: ( <.p.) c= H & H is being_ultrafilter ) by A2, Th18, Th19;
take  H ; ::_thesis: ( p in H & H is being_ultrafilter )
 p in <.p.) ;
hence  ( p in H & H is being_ultrafilter ) by A3; ::_thesis: verum
end;

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 & ( 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 & ( for F being Filter of L st D c= F holds
b1 c= F ) )
proof
set x = the Element of D;
defpred S1[ set ] means ( $1 is Filter of L & D c= $1 );
consider X being set  such that
A1: for Z being set holds
( Z in X iff ( Z in bool the carrier of L & S1[Z] ) ) from XBOOLE_0:sch_1();
reconsider x = the Element of D as Element of L ;
 <.L.) = the carrier of L ;
then A2: X <> {} by A1;
now__::_thesis:_for_Z_being_set_st_Z_in_X_holds_
x_in_Z
let Z be set ; ::_thesis: ( Z in X implies x in Z )
assume  Z in X ; ::_thesis: x in Z
then  D c= Z by A1;
hence  x in Z by TARSKI:def_3; ::_thesis: verum
end;
then reconsider F = meet X as non empty set by A2, SETFAM_1:def_1;
A3: <.L.) in X by A1;
 F c= the carrier of L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F or x in the carrier of L )
thus  ( not x in F or x in the carrier of L ) by A3, SETFAM_1:def_1; ::_thesis: verum
end;
then reconsider F = F as non empty Subset of L ;
now__::_thesis:_for_p,_q_being_Element_of_L_holds_
(_(_p_in_F_&_q_in_F_implies_p_"/\"_q_in_F_)_&_(_p_"/\"_q_in_F_implies_(_p_in_F_&_q_in_F_)_)_)
let p, q be Element of L; ::_thesis: ( ( p in F & q in F implies p "/\" q in F ) & ( p "/\" q in F implies ( p in F & q in F ) ) )
thus  ( p in F & q in F implies p "/\" q in F ) ::_thesis: ( p "/\" q in F implies ( p in F & q in F ) )
proof
assume A4: ( p in F & q in F ) ; ::_thesis: p "/\" q in F
 for Z being set st Z in X holds
p "/\" q in Z
proof
let Z be set ; ::_thesis: ( Z in X implies p "/\" q in Z )
assume A5: Z in X ; ::_thesis: p "/\" q in Z
then reconsider Z9 = Z as Filter of L by A1;
 ( p in Z9 & q in Z9 ) by A4, A5, SETFAM_1:def_1;
hence  p "/\" q in Z by Th8; ::_thesis: verum
end;
hence  p "/\" q in F by A2, SETFAM_1:def_1; ::_thesis: verum
end;
assume A6: p "/\" q in F ; ::_thesis: ( p in F & q in F )
now__::_thesis:_for_Z_being_set_st_Z_in_X_holds_
p_in_Z
let Z be set ; ::_thesis: ( Z in X implies p in Z )
assume A7: Z in X ; ::_thesis: p in Z
then reconsider Z9 = Z as Filter of L by A1;
 p "/\" q in Z9 by A6, A7, SETFAM_1:def_1;
hence  p in Z by Th8; ::_thesis: verum
end;
hence  p in F by A2, SETFAM_1:def_1; ::_thesis: q in F
now__::_thesis:_for_Z_being_set_st_Z_in_X_holds_
q_in_Z
let Z be set ; ::_thesis: ( Z in X implies q in Z )
assume A8: Z in X ; ::_thesis: q in Z
then reconsider Z9 = Z as Filter of L by A1;
 p "/\" q in Z9 by A6, A8, SETFAM_1:def_1;
hence  q in Z by Th8; ::_thesis: verum
end;
hence  q in F by A2, SETFAM_1:def_1; ::_thesis: verum
end;
then reconsider F = F as Filter of L by Th8;
take  F ; ::_thesis: ( D c= F & ( for F being Filter of L st D c= F holds
F c= F ) )
 for Z being set st Z in X holds
D c= Z by A1;
hence  D c= F by A2, SETFAM_1:5; ::_thesis: for F being Filter of L st D c= F holds
F c= F
let H be Filter of L; ::_thesis: ( D c= H implies F c= H )
assume  D c= H ; ::_thesis: F c= H
then  H in X by A1;
hence  F c= H by SETFAM_1:3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Filter of L st D c= b1 & ( for F being Filter of L st D c= F holds
b1 c= F ) & D c= b2 & ( for F being Filter of L st D c= F holds
b2 c= F ) holds
b1 = b2
proof
let F1, F2 be Filter of L; ::_thesis: ( D c= F1 & ( for F being Filter of L st D c= F holds
F1 c= F ) & D c= F2 & ( for F being Filter of L st D c= F holds
F2 c= F ) implies F1 = F2 )
assume  ( D c= F1 & ( for F being Filter of L st D c= F holds
F1 c= F ) & D c= F2 & ( for F being Filter of L st D c= F holds
F2 c= F ) ) ; ::_thesis: F1 = F2
hence  ( F1 c= F2 & F2 c= F1 ) ; :: according to XBOOLE_0:def_10 ::_thesis: verum
end;
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 & ( 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
proof
let L be Lattice; ::_thesis: for F being Filter of L holds <.F.) = F
let F be Filter of L; ::_thesis: <.F.) = F
 for H being Filter of L st F c= H holds
F c= H ;
hence  <.F.) = F by Def4; ::_thesis: verum
end;


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.)
proof
let L be Lattice; ::_thesis: for D1, D2 being non empty Subset of L st D1 c= D2 holds
<.D1.) c= <.D2.)
let D1, D2 be non empty Subset of L; ::_thesis: ( D1 c= D2 implies <.D1.) c= <.D2.) )
assume A1: D1 c= D2 ; ::_thesis: <.D1.) c= <.D2.)
 D2 c= <.D2.) by Def4;
then  D1 c= <.D2.) by A1, XBOOLE_1:1;
hence  <.D1.) c= <.D2.) by Def4; ::_thesis: verum
end;

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.)
proof
let L be Lattice; ::_thesis: for p being Element of L
for D being non empty Subset of L st p in D holds
<.p.) c= <.D.)
let p be Element of L; ::_thesis: for D being non empty Subset of L st p in D holds
<.p.) c= <.D.)
let D be non empty Subset of L; ::_thesis: ( p in D implies <.p.) c= <.D.) )
assume A1: p in D ; ::_thesis: <.p.) c= <.D.)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in <.p.) or x in <.D.) )
A2: D c= <.D.) by Def4;
assume  x in <.p.) ; ::_thesis: x in <.D.)
then  ex q being Element of L st
( x = q & p [= q ) ;
hence  x in <.D.) by A1, A2, Th9; ::_thesis: verum
end;

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.)
proof
let L be Lattice; ::_thesis: for p being Element of L
for D being non empty Subset of L st D = {p} holds
<.D.) = <.p.)
let p be Element of L; ::_thesis: for D being non empty Subset of L st D = {p} holds
<.D.) = <.p.)
let D be non empty Subset of L; ::_thesis: ( D = {p} implies <.D.) = <.p.) )
assume A1: D = {p} ; ::_thesis: <.D.) = <.p.)
 D c= <.p.)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D or x in <.p.) )
assume  x in D ; ::_thesis: x in <.p.)
then  x = p by A1, TARSKI:def_1;
hence  x in <.p.) ; ::_thesis: verum
end;
hence  <.D.) c= <.p.) by Def4; :: according to XBOOLE_0:def_10 ::_thesis: <.p.) c= <.D.)
 p in D by A1, TARSKI:def_1;
hence  <.p.) c= <.D.) by Th23; ::_thesis: verum
end;

theorem Th25: :: FILTER_0:25
for L being Lattice
for D being non empty Subset of L st L is 0_Lattice & Bottom L in D holds
( <.D.) = <.L.) & <.D.) = the carrier of L )
proof
let L be Lattice; ::_thesis: for D being non empty Subset of L st L is 0_Lattice & Bottom L in D holds
( <.D.) = <.L.) & <.D.) = the carrier of L )
let D be non empty Subset of L; ::_thesis: ( L is 0_Lattice & Bottom L in D implies ( <.D.) = <.L.) & <.D.) = the carrier of L ) )
assume that
A1: L is 0_Lattice and
A2: Bottom L in D ; ::_thesis: ( <.D.) = <.L.) & <.D.) = the carrier of L )
A3: <.(Bottom L).) = <.L.) by A1, Th17;
hence  ( <.D.) c= <.L.) & <.L.) c= <.D.) ) by A2, Th23; :: according to XBOOLE_0:def_10 ::_thesis: <.D.) = the carrier of L
thus  ( <.D.) c= the carrier of L & the carrier of L c= <.D.) ) by A2, A3, Th23; :: according to XBOOLE_0:def_10 ::_thesis: verum
end;

theorem Th26: :: FILTER_0:26
for L being Lattice
for F being Filter of L st L is 0_Lattice & Bottom L in F holds
( F = <.L.) & F = the carrier of L )
proof
let L be Lattice; ::_thesis: for F being Filter of L st L is 0_Lattice & Bottom L in F holds
( F = <.L.) & F = the carrier of L )
let F be Filter of L; ::_thesis: ( L is 0_Lattice & Bottom L in F implies ( F = <.L.) & F = the carrier of L ) )
 F = <.F.) by Th21;
hence  ( L is 0_Lattice & Bottom L in F implies ( F = <.L.) & F = the carrier of L ) ) by Th25; ::_thesis: verum
end;

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 & ( for r being Element of L st p "/\" r [= q holds
r [= (p `) "\/" q ) )
proof
let L be Lattice; ::_thesis: ( L is B_Lattice implies for p, q being Element of L holds
( p "/\" ((p `) "\/" q) [= q & ( for r being Element of L st p "/\" r [= q holds
r [= (p `) "\/" q ) ) )
assume  L is B_Lattice ; ::_thesis: for p, q being Element of L holds
( p "/\" ((p `) "\/" q) [= q & ( for r being Element of L st p "/\" r [= q holds
r [= (p `) "\/" q ) )
then reconsider S = L as B_Lattice ;
reconsider J = S as 1_Lattice ;
reconsider K = S as 0_Lattice ;
let p, q be Element of L; ::_thesis: ( p "/\" ((p `) "\/" q) [= q & ( for r being Element of L st p "/\" r [= q holds
r [= (p `) "\/" q ) )
set r = (p `) "\/" q;
reconsider p9 = p, q9 = q as Element of K ;
reconsider p99 = p as Element of S ;
A1: ( p99 "/\" (p99 `) = Bottom L & (Bottom K) "\/" (p9 "/\" q9) = p9 "/\" q9 ) by LATTICES:20;
reconsider K = S as D_Lattice ;
reconsider p9 = p, q9 = q, r9 = (p `) "\/" q as Element of K ;
 p9 "/\" r9 = (p9 "/\" (p9 `)) "\/" (p9 "/\" q9) by LATTICES:def_11;
hence  p "/\" ((p `) "\/" q) [= q by A1, LATTICES:6; ::_thesis: for r being Element of L st p "/\" r [= q holds
r [= (p `) "\/" q
let r1 be Element of L; ::_thesis: ( p "/\" r1 [= q implies r1 [= (p `) "\/" q )
reconsider r19 = r1 as Element of K ;
reconsider pp = p, r99 = r1 as Element of J ;
A2: ( (p99 `) "\/" p99 = Top L & (Top J) "/\" ((pp `) "\/" r99) = (pp `) "\/" r99 ) by LATTICES:21;
assume  p "/\" r1 [= q ; ::_thesis: r1 [= (p `) "\/" q
then A3: (p `) "\/" (p "/\" r1) [= (p `) "\/" q by Th1;
 ( (p9 `) "\/" (p9 "/\" r19) = ((p9 `) "\/" p9) "/\" ((p9 `) "\/" r19) & r1 [= r1 "\/" (p `) ) by LATTICES:5, LATTICES:11;
hence  r1 [= (p `) "\/" q by A3, A2, LATTICES:7; ::_thesis: verum
end;

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 & ( 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 & ( 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 & b1 is implicative )
proof
set L = the strict B_Lattice;
now__::_thesis:_for_p,_q_being_Element_of_the_strict_B_Lattice_ex_r_being_Element_of_the_strict_B_Lattice_st_
(_p_"/\"_r_[=_q_&_(_for_r1_being_Element_of_the_strict_B_Lattice_st_p_"/\"_r1_[=_q_holds_
r1_[=_r_)_)
let p, q be Element of the strict B_Lattice; ::_thesis: ex r being Element of the strict B_Lattice st
( p "/\" r [= q & ( for r1 being Element of the strict B_Lattice st p "/\" r1 [= q holds
r1 [= r ) )
reconsider r = (p `) "\/" q as Element of the strict B_Lattice ;
take r = r; ::_thesis: ( p "/\" r [= q & ( for r1 being Element of the strict B_Lattice st p "/\" r1 [= q holds
r1 [= r ) )
thus  ( p "/\" r [= q & ( for r1 being Element of the strict B_Lattice st p "/\" r1 [= q holds
r1 [= r ) ) by Th27; ::_thesis: verum
end;
then  the strict B_Lattice is implicative by Def6;
hence  ex b1 being Lattice st
( b1 is strict & b1 is implicative ) ; ::_thesis: verum
end;
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 & ( for r being Element of L st p "/\" r [= q holds
r [= it ) );
existence
 ex b1 being Element of L st
( p "/\" b1 [= q & ( 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 & ( for r being Element of L st p "/\" r [= q holds
r [= b1 ) & p "/\" b2 [= q & ( for r being Element of L st p "/\" r [= q holds
r [= b2 ) holds
b1 = b2;
proof
let r1, r2 be Element of L; ::_thesis: ( p "/\" r1 [= q & ( for r being Element of L st p "/\" r [= q holds
r [= r1 ) & p "/\" r2 [= q & ( for r being Element of L st p "/\" r [= q holds
r [= r2 ) implies r1 = r2 )
assume  ( p "/\" r1 [= q & ( for r being Element of L st p "/\" r [= q holds
r [= r1 ) & p "/\" r2 [= q & ( for r being Element of L st p "/\" r [= q holds
r [= r2 ) ) ; ::_thesis: r1 = r2
then  ( r1 [= r2 & r2 [= r1 ) ;
hence  r1 = r2 by LATTICES:8; ::_thesis: verum
end;
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 & ( 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
proof
let I be I_Lattice; ::_thesis: I is upper-bounded
set i = the Element of I;
take k = the Element of I => the Element of I; :: according to LATTICES:def_14 ::_thesis: for b1 being Element of the carrier of I holds
( k "\/" b1 = k & b1 "\/" k = k )
let j be Element of I; ::_thesis: ( k "\/" j = k & j "\/" k = k )
 the Element of I "/\" j [= the Element of I by LATTICES:6;
then A1: j [= k by Def7;
 j "\/" k = k "\/" j ;
hence  ( k "\/" j = k & j "\/" k = k ) by A1, LATTICES:def_3; ::_thesis: verum
end;
end;

theorem Th28: :: FILTER_0:28
for I being I_Lattice
for i being Element of I holds i => i = Top I
proof
let I be I_Lattice; ::_thesis: for i being Element of I holds i => i = Top I
let i be Element of I; ::_thesis: i => i = Top I
now__::_thesis:_for_j_being_Element_of_I_holds_j_"\/"_(i_=>_i)_=_i_=>_i
let j be Element of I; ::_thesis: j "\/" (i => i) = i => i
 i "/\" j [= i by LATTICES:6;
then  j [= i => i by Def7;
hence  j "\/" (i => i) = i => i by LATTICES:def_3; ::_thesis: verum
end;
hence  i => i = Top I by RLSUB_2:65; ::_thesis: verum
end;

registration
cluster non empty Lattice-like implicative  ->  distributive for LattStr ;
coherence
 for b1 being I_Lattice holds b1 is distributive
proof
let I be I_Lattice; ::_thesis: I is distributive
let i be Element of I; :: according to LATTICES:def_11 ::_thesis: for b1, b2 being Element of the carrier of I holds i "/\" (b1 "\/" b2) = (i "/\" b1) "\/" (i "/\" b2)
let j, k be Element of I; ::_thesis: i "/\" (j "\/" k) = (i "/\" j) "\/" (i "/\" k)
 i "/\" k [= (i "/\" k) "\/" (i "/\" j) by LATTICES:5;
then A1: k [= i => ((i "/\" j) "\/" (i "/\" k)) by Def7;
 i "/\" j [= (i "/\" j) "\/" (i "/\" k) by LATTICES:5;
then  j [= i => ((i "/\" j) "\/" (i "/\" k)) by Def7;
then  j "\/" k [= i => ((i "/\" j) "\/" (i "/\" k)) by A1, Th6;
then A2: i "/\" (j "\/" k) [= i "/\" (i => ((i "/\" j) "\/" (i "/\" k))) by LATTICES:9;
 ( i "/\" j [= i "/\" (j "\/" k) & i "/\" k [= i "/\" (j "\/" k) ) by LATTICES:5, LATTICES:9;
then A3: (i "/\" j) "\/" (i "/\" k) [= i "/\" (j "\/" k) by Th6;
 i "/\" (i => ((i "/\" j) "\/" (i "/\" k))) [= (i "/\" j) "\/" (i "/\" k) by Def7;
then  i "/\" (j "\/" k) [= (i "/\" j) "\/" (i "/\" k) by A2, LATTICES:7;
hence  i "/\" (j "\/" k) = (i "/\" j) "\/" (i "/\" k) by A3, LATTICES:8; ::_thesis: verum
end;
end;


registration
cluster non empty Lattice-like Boolean  ->  implicative for LattStr ;
coherence
 for b1 being B_Lattice holds b1 is implicative
proof
let B be B_Lattice; ::_thesis: B is implicative
let p, q be Element of B; :: according to FILTER_0:def_6 ::_thesis: ex r being Element of B st
( p "/\" r [= q & ( for r1 being Element of B st p "/\" r1 [= q holds
r1 [= r ) )
take r = (p `) "\/" q; ::_thesis: ( p "/\" r [= q & ( for r1 being Element of B st p "/\" r1 [= q holds
r1 [= r ) )
thus  ( p "/\" r [= q & ( for r1 being Element of B st p "/\" r1 [= q holds
r1 [= r ) ) by Th27; ::_thesis: verum
end;
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 & i => j in FI holds
j in FI
proof
let I be I_Lattice; ::_thesis: for i, j being Element of I
for FI being Filter of I st i in FI & i => j in FI holds
j in FI
let i, j be Element of I; ::_thesis: for FI being Filter of I st i in FI & i => j in FI holds
j in FI
let FI be Filter of I; ::_thesis: ( i in FI & i => j in FI implies j in FI )
assume  ( i in FI & i => j in FI ) ; ::_thesis: j in FI
then A1: i "/\" (i => j) in FI by Th8;
 i "/\" (i => j) [= j by Def7;
hence  j in FI by A1, Th9; ::_thesis: verum
end;

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
proof
let I be I_Lattice; ::_thesis: for j, i being Element of I
for FI being Filter of I st j in FI holds
i => j in FI
let j, i be Element of I; ::_thesis: for FI being Filter of I st j in FI holds
i => j in FI
let FI be Filter of I; ::_thesis: ( j in FI implies i => j in FI )
 j "/\" i [= j by LATTICES:6;
then  j [= i => j by Def7;
hence  ( j in FI implies i => j in FI ) by Th9; ::_thesis: verum
end;

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 & q in D2 )  }  ;
coherence
  {  (p "/\" q) where p, q is Element of L : ( p in D1 & q in D2 )  }  is Subset of L
proof
set x = the Element of D1;
set y = the Element of D2;
reconsider x = the Element of D1, y = the Element of D2 as Element of L ;
 x "/\" y in  {  (p "/\" q) where p, q is Element of L : ( p in D1 & q in D2 )  }  ;
then reconsider D =  {  (p "/\" q) where p, q is Element of L : ( p in D1 & q in D2 )  }  as non empty set ;
 D c= the carrier of L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D or x in the carrier of L )
assume  x in D ; ::_thesis: x in the carrier of L
then  ex p, q being Element of L st
( x = p "/\" q & p in D1 & q in D2 ) ;
hence  x in the carrier of L ; ::_thesis: verum
end;
hence   {  (p "/\" q) where p, q is Element of L : ( p in D1 & q in D2 )  }  is Subset of L ; ::_thesis: verum
end;
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 & 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
proof
set x = the Element of D1;
set y = the Element of D2;
reconsider x = the Element of D1, y = the Element of D2 as Element of L ;
 x "/\" y in  {  (p "/\" q) where p, q is Element of L : ( p in D1 & q in D2 )  }  ;
hence  not D1 "/\" D2 is empty ; ::_thesis: verum
end;
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 & q in D2 holds
( p "/\" q in D1 "/\" D2 & 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 & p in D1 & 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
proof
let L be Lattice; ::_thesis: for D1, D2 being non empty Subset of L holds D1 "/\" D2 = D2 "/\" D1
let D1, D2 be non empty Subset of L; ::_thesis: D1 "/\" D2 = D2 "/\" D1
now__::_thesis:_for_D1,_D2_being_non_empty_Subset_of_L_holds_D1_"/\"_D2_c=_D2_"/\"_D1
let D1, D2 be non empty Subset of L; ::_thesis: D1 "/\" D2 c= D2 "/\" D1
thus  D1 "/\" D2 c= D2 "/\" D1 ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D1 "/\" D2 or x in D2 "/\" D1 )
assume  x in D1 "/\" D2 ; ::_thesis: x in D2 "/\" D1
then  ex p, q being Element of L st
( x = p "/\" q & p in D1 & q in D2 ) ;
hence  x in D2 "/\" D1 ; ::_thesis: verum
end;
end;
hence  ( D1 "/\" D2 c= D2 "/\" D1 & D2 "/\" D1 c= D1 "/\" D2 ) ; :: according to XBOOLE_0:def_10 ::_thesis: verum
end;

registration
let L be D_Lattice;
let F1, F2 be Filter of L;
clusterF1 "/\" F2 ->  final meet-closed ;
coherence
 ( F1 "/\" F2 is final & F1 "/\" F2 is meet-closed )
proof
now__::_thesis:_for_p,_q_being_Element_of_L_holds_
(_(_p_in_F1_"/\"_F2_&_q_in_F1_"/\"_F2_implies_p_"/\"_q_in_F1_"/\"_F2_)_&_(_p_"/\"_q_in_F1_"/\"_F2_implies_(_p_in_F1_"/\"_F2_&_q_in_F1_"/\"_F2_)_)_)
let p, q be Element of L; ::_thesis: ( ( p in F1 "/\" F2 & q in F1 "/\" F2 implies p "/\" q in F1 "/\" F2 ) & ( p "/\" q in F1 "/\" F2 implies ( p in F1 "/\" F2 & q in F1 "/\" F2 ) ) )
A1: ( p = p "\/" (p "/\" q) & q = q "\/" (p "/\" q) ) by LATTICES:def_8;
thus  ( p in F1 "/\" F2 & q in F1 "/\" F2 implies p "/\" q in F1 "/\" F2 ) ::_thesis: ( p "/\" q in F1 "/\" F2 implies ( p in F1 "/\" F2 & q in F1 "/\" F2 ) )
proof
assume  p in F1 "/\" F2 ; ::_thesis: ( not q in F1 "/\" F2 or p "/\" q in F1 "/\" F2 )
then consider p1, p2 being Element of L such that
A2: p = p1 "/\" p2 and
A3: ( p1 in F1 & p2 in F2 ) ;
assume  q in F1 "/\" F2 ; ::_thesis: p "/\" q in F1 "/\" F2
then consider q1, q2 being Element of L such that
A4: q = q1 "/\" q2 and
A5: ( q1 in F1 & q2 in F2 ) ;
A6: p "/\" q = ((p1 "/\" p2) "/\" q1) "/\" q2 by A2, A4, LATTICES:def_7
.= ((p1 "/\" q1) "/\" p2) "/\" q2 by LATTICES:def_7
.= (p1 "/\" q1) "/\" (p2 "/\" q2) by LATTICES:def_7 ;
 ( p1 "/\" q1 in F1 & p2 "/\" q2 in F2 ) by A3, A5, Th8;
hence  p "/\" q in F1 "/\" F2 by A6; ::_thesis: verum
end;
assume  p "/\" q in F1 "/\" F2 ; ::_thesis: ( p in F1 "/\" F2 & q in F1 "/\" F2 )
then consider p1, q1 being Element of L such that
A7: p "/\" q = p1 "/\" q1 and
A8: ( p1 in F1 & q1 in F2 ) ;
A9: ( q "\/" p1 in F1 & q "\/" q1 in F2 ) by A8, Th10;
A10: ( p "\/" (p1 "/\" q1) = (p "\/" p1) "/\" (p "\/" q1) & q "\/" (p1 "/\" q1) = (q "\/" p1) "/\" (q "\/" q1) ) by LATTICES:11;
 ( p "\/" p1 in F1 & p "\/" q1 in F2 ) by A8, Th10;
hence  ( p in F1 "/\" F2 & q in F1 "/\" F2 ) by A7, A1, A10, A9; ::_thesis: verum
end;
hence  ( F1 "/\" F2 is final & F1 "/\" F2 is meet-closed ) by Th8; ::_thesis: verum
end;
end;

theorem Th34: :: FILTER_0:34
for L being Lattice
for D1, D2 being non empty Subset of L holds
( <.(D1 \/ D2).) = <.(<.D1.) \/ D2).) & <.(D1 \/ D2).) = <.(D1 \/ <.D2.)).) )
proof
let L be Lattice; ::_thesis: for D1, D2 being non empty Subset of L holds
( <.(D1 \/ D2).) = <.(<.D1.) \/ D2).) & <.(D1 \/ D2).) = <.(D1 \/ <.D2.)).) )
let D1, D2 be non empty Subset of L; ::_thesis: ( <.(D1 \/ D2).) = <.(<.D1.) \/ D2).) & <.(D1 \/ D2).) = <.(D1 \/ <.D2.)).) )
now__::_thesis:_for_D1,_D2_being_non_empty_Subset_of_L_holds_
(_<.(D1_\/_D2).)_c=_<.(<.D1.)_\/_D2).)_&_<.(<.D1.)_\/_D2).)_c=_<.(D1_\/_D2).)_)
let D1, D2 be non empty Subset of L; ::_thesis: ( <.(D1 \/ D2).) c= <.(<.D1.) \/ D2).) & <.(<.D1.) \/ D2).) c= <.(D1 \/ D2).) )
 ( D2 c= D1 \/ D2 & D1 \/ D2 c= <.(D1 \/ D2).) ) by Def4, XBOOLE_1:7;
then A1: D2 c= <.(D1 \/ D2).) by XBOOLE_1:1;
 D1 c= <.D1.) by Def4;
then  D1 \/ D2 c= <.D1.) \/ D2 by XBOOLE_1:9;
hence  <.(D1 \/ D2).) c= <.(<.D1.) \/ D2).) by Th22; ::_thesis: <.(<.D1.) \/ D2).) c= <.(D1 \/ D2).)
 <.D1.) c= <.(D1 \/ D2).) by Th22, XBOOLE_1:7;
then  <.D1.) \/ D2 c= <.(D1 \/ D2).) by A1, XBOOLE_1:8;
hence  <.(<.D1.) \/ D2).) c= <.(D1 \/ D2).) by Def4; ::_thesis: verum
end;
hence  ( <.(D1 \/ D2).) c= <.(<.D1.) \/ D2).) & <.(<.D1.) \/ D2).) c= <.(D1 \/ D2).) & <.(D1 \/ D2).) c= <.(D1 \/ <.D2.)).) & <.(D1 \/ <.D2.)).) c= <.(D1 \/ D2).) ) ; :: according to XBOOLE_0:def_10 ::_thesis: verum
end;

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 & p in F & q in H )  }
proof
let L be Lattice; ::_thesis: 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 & p in F & q in H )  }
let F, H be Filter of L; ::_thesis: <.(F \/ H).) =  {  r where r is Element of L : ex p, q being Element of L st
( p "/\" q [= r & p in F & q in H )  }
set X =  {  r1 where r1 is Element of L : ex p, q being Element of L st
( p "/\" q [= r1 & p in F & q in H )  }  ;
consider p1 being Element of L such that
A1: p1 in F by SUBSET_1:4;
consider q1 being Element of L such that
A2: q1 in H by SUBSET_1:4;
 p1 "/\" q1 in  {  r1 where r1 is Element of L : ex p, q being Element of L st
( p "/\" q [= r1 & p in F & q in H )  }  by A1, A2;
then reconsider D =  {  r1 where r1 is Element of L : ex p, q being Element of L st
( p "/\" q [= r1 & p in F & q in H )  }  as non empty set ;
 D c= the carrier of L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D or x in the carrier of L )
assume  x in D ; ::_thesis: x in the carrier of L
then  ex r1 being Element of L st
( x = r1 & ex p, q being Element of L st
( p "/\" q [= r1 & p in F & q in H ) ) ;
hence  x in the carrier of L ; ::_thesis: verum
end;
then reconsider D = D as non empty Subset of L ;
A3: for p, q being Element of L st p in D & p [= q holds
q in D
proof
let p, q be Element of L; ::_thesis: ( p in D & p [= q implies q in D )
assume  p in D ; ::_thesis: ( not p [= q or q in D )
then  ex r1 being Element of L st
( p = r1 & ex p, q being Element of L st
( p "/\" q [= r1 & p in F & q in H ) ) ;
then consider p1, q1 being Element of L such that
A4: p1 "/\" q1 [= p and
A5: ( p1 in F & q1 in H ) ;
assume  p [= q ; ::_thesis: q in D
then  p1 "/\" q1 [= q by A4, LATTICES:7;
hence  q in D by A5; ::_thesis: verum
end;
 for p, q being Element of L st p in D & q in D holds
p "/\" q in D
proof
let p, q be Element of L; ::_thesis: ( p in D & q in D implies p "/\" q in D )
assume  p in D ; ::_thesis: ( not q in D or p "/\" q in D )
then  ex r1 being Element of L st
( p = r1 & ex p, q being Element of L st
( p "/\" q [= r1 & p in F & q in H ) ) ;
then consider p1, q1 being Element of L such that
A6: p1 "/\" q1 [= p and
A7: ( p1 in F & q1 in H ) ;
assume  q in D ; ::_thesis: p "/\" q in D
then  ex r2 being Element of L st
( q = r2 & ex p, q being Element of L st
( p "/\" q [= r2 & p in F & q in H ) ) ;
then consider p2, q2 being Element of L such that
A8: p2 "/\" q2 [= q and
A9: ( p2 in F & q2 in H ) ;
A10: p "/\" (p2 "/\" q2) [= p "/\" q by A8, LATTICES:9;
 (p1 "/\" q1) "/\" (p2 "/\" q2) [= p "/\" (p2 "/\" q2) by A6, LATTICES:9;
then A11: (p1 "/\" q1) "/\" (p2 "/\" q2) [= p "/\" q by A10, LATTICES:7;
A12: (p1 "/\" q1) "/\" (p2 "/\" q2) = ((p1 "/\" q1) "/\" p2) "/\" q2 by LATTICES:def_7
.= ((p1 "/\" p2) "/\" q1) "/\" q2 by LATTICES:def_7
.= (p1 "/\" p2) "/\" (q1 "/\" q2) by LATTICES:def_7 ;
 ( p1 "/\" p2 in F & q1 "/\" q2 in H ) by A7, A9, Th8;
hence  p "/\" q in D by A12, A11; ::_thesis: verum
end;
then reconsider D = D as Filter of L by A3, Th9;
A13: H c= D
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in H or x in D )
assume  x in H ; ::_thesis: x in D
then reconsider q = x as Element of H ;
 q "/\" p1 [= q by LATTICES:6;
hence  x in D by A1; ::_thesis: verum
end;
 F c= D
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F or x in D )
assume  x in F ; ::_thesis: x in D
then reconsider p = x as Element of F ;
 p "/\" q1 [= p by LATTICES:6;
hence  x in D by A2; ::_thesis: verum
end;
then  F \/ H c= D by A13, XBOOLE_1:8;
hence  <.(F \/ H).) c=  {  r1 where r1 is Element of L : ex p, q being Element of L st
( p "/\" q [= r1 & p in F & q in H )  }  by Def4; :: according to XBOOLE_0:def_10 ::_thesis:  {  r where r is Element of L : ex p, q being Element of L st
( p "/\" q [= r & p in F & q in H )  }  c= <.(F \/ H).)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  r where r is Element of L : ex p, q being Element of L st
( p "/\" q [= r & p in F & q in H )  }  or x in <.(F \/ H).) )
assume  x in  {  r1 where r1 is Element of L : ex p, q being Element of L st
( p "/\" q [= r1 & p in F & q in H )  }  ; ::_thesis: x in <.(F \/ H).)
then consider r being Element of L such that
A14: x = r and
A15: ex p, q being Element of L st
( p "/\" q [= r & p in F & q in H ) ;
A16: F \/ H c= <.(F \/ H).) by Def4;
 H c= F \/ H by XBOOLE_1:7;
then A17: H c= <.(F \/ H).) by A16, XBOOLE_1:1;
consider p, q being Element of L such that
A18: p "/\" q [= r and
A19: ( p in F & q in H ) by A15;
 F c= F \/ H by XBOOLE_1:7;
then  F c= <.(F \/ H).) by A16, XBOOLE_1:1;
then  p "/\" q in <.(F \/ H).) by A19, A17, Th8;
hence  x in <.(F \/ H).) by A14, A18, Th9; ::_thesis: verum
end;

theorem Th36: :: FILTER_0:36
for L being Lattice
for F, H being Filter of L holds
( F c= F "/\" H & H c= F "/\" H )
proof
let L be Lattice; ::_thesis: for F, H being Filter of L holds
( F c= F "/\" H & H c= F "/\" H )
let F, H be Filter of L; ::_thesis: ( F c= F "/\" H & H c= F "/\" H )
A1: now__::_thesis:_for_F,_H_being_Filter_of_L_holds_F_c=_F_"/\"_H
let F, H be Filter of L; ::_thesis: F c= F "/\" H
thus  F c= F "/\" H ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F or x in F "/\" H )
assume A2: x in F ; ::_thesis: x in F "/\" H
then reconsider i = x as Element of L ;
consider p being Element of L such that
A3: p in H by SUBSET_1:4;
 i [= i "\/" p by LATTICES:5;
then A4: i "/\" (i "\/" p) = i by LATTICES:4;
 p [= p "\/" i by LATTICES:5;
then  i "\/" p in H by A3, Th9;
hence  x in F "/\" H by A2, A4; ::_thesis: verum
end;
end;
 F "/\" H = H "/\" F by Th33;
hence  ( F c= F "/\" H & H c= F "/\" H ) by A1; ::_thesis: verum
end;

theorem Th37: :: FILTER_0:37
for L being Lattice
for F, H being Filter of L holds <.(F \/ H).) = <.(F "/\" H).)
proof
let L be Lattice; ::_thesis: for F, H being Filter of L holds <.(F \/ H).) = <.(F "/\" H).)
let F, H be Filter of L; ::_thesis: <.(F \/ H).) = <.(F "/\" H).)
 ( F c= F "/\" H & H c= F "/\" H ) by Th36;
then  F \/ H c= F "/\" H by XBOOLE_1:8;
hence  <.(F \/ H).) c= <.(F "/\" H).) by Th22; :: according to XBOOLE_0:def_10 ::_thesis: <.(F "/\" H).) c= <.(F \/ H).)
 F "/\" H c= <.(F \/ H).)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F "/\" H or x in <.(F \/ H).) )
assume  x in F "/\" H ; ::_thesis: x in <.(F \/ H).)
then consider p, q being Element of L such that
A1: x = p "/\" q and
A2: p in F and
A3: q in H ;
 H c= F \/ H by XBOOLE_1:7;
then A4: q in F \/ H by A3;
A5: F \/ H c= <.(F \/ H).) by Def4;
 F c= F \/ H by XBOOLE_1:7;
then  p in F \/ H by A2;
hence  x in <.(F \/ H).) by A1, A4, A5, Th9; ::_thesis: verum
end;
then  <.(F "/\" H).) c= <.<.(F \/ H).).) by Th22;
hence  <.(F "/\" H).) c= <.(F \/ H).) by Th21; ::_thesis: verum
end;


theorem Th38: :: FILTER_0:38
for I being I_Lattice
for F1, F2 being Filter of I holds <.(F1 \/ F2).) = F1 "/\" F2
proof
let I be I_Lattice; ::_thesis: for F1, F2 being Filter of I holds <.(F1 \/ F2).) = F1 "/\" F2
let F1, F2 be Filter of I; ::_thesis: <.(F1 \/ F2).) = F1 "/\" F2
 F1 "/\" F2 = <.(F1 "/\" F2).) by Th21;
hence  <.(F1 \/ F2).) = F1 "/\" F2 by Th37; ::_thesis: verum
end;

theorem :: FILTER_0:39
for B being B_Lattice
for FB, HB being Filter of B holds <.(FB \/ HB).) = FB "/\" HB
proof
let B be B_Lattice; ::_thesis: for FB, HB being Filter of B holds <.(FB \/ HB).) = FB "/\" HB
let FB, HB be Filter of B; ::_thesis: <.(FB \/ HB).) = FB "/\" HB
 FB "/\" HB = <.(FB "/\" HB).) by Th21;
hence  <.(FB \/ HB).) = FB "/\" HB by Th37; ::_thesis: verum
end;

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.)
proof
let I be I_Lattice; ::_thesis: 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.)
let j, i be Element of I; ::_thesis: for DI being non empty Subset of I st j in <.(DI \/ {i}).) holds
i => j in <.DI.)
let DI be non empty Subset of I; ::_thesis: ( j in <.(DI \/ {i}).) implies i => j in <.DI.) )
assume A1: j in <.(DI \/ {i}).) ; ::_thesis: i => j in <.DI.)
<.(DI \/ {i}).) = <.(<.DI.) \/ {i}).) by Th34
.= <.(<.DI.) \/ <.{i}.)).) by Th34
.= <.(<.DI.) \/ <.i.)).) by Th24
.= <.DI.) "/\" <.i.) by Th38 ;
then consider i1, i2 being Element of I such that
A2: j = i1 "/\" i2 and
A3: i1 in <.DI.) and
A4: i2 in <.i.) by A1;
 i [= i2 by A4, Th15;
then  i1 "/\" i [= i1 "/\" i2 by LATTICES:9;
then  i1 [= i => j by A2, Def7;
hence  i => j in <.DI.) by A3, Th9; ::_thesis: verum
end;

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 & j => k in FI holds
i => k in FI
proof
let I be I_Lattice; ::_thesis: for i, j, k being Element of I
for FI being Filter of I st i => j in FI & j => k in FI holds
i => k in FI
let i, j, k be Element of I; ::_thesis: for FI being Filter of I st i => j in FI & j => k in FI holds
i => k in FI
let FI be Filter of I; ::_thesis: ( i => j in FI & j => k in FI implies i => k in FI )
assume that
A1: i => j in FI and
A2: j => k in FI ; ::_thesis: i => k in FI
A3: FI \/ {i} c= <.(FI \/ {i}).) by Def4;
 {i} c= FI \/ {i} by XBOOLE_1:7;
then A4: {i} c= <.(FI \/ {i}).) by A3, XBOOLE_1:1;
 FI c= FI \/ {i} by XBOOLE_1:7;
then A5: FI c= <.(FI \/ {i}).) by A3, XBOOLE_1:1;
 i in {i} by TARSKI:def_1;
then  j in <.(FI \/ {i}).) by A1, A5, A4, Th29;
then A6: k in <.(FI \/ {i}).) by A2, A5, Th29;
 <.FI.) = FI by Th21;
hence  i => k in FI by A6, Th40; ::_thesis: verum
end;


theorem Th42: :: FILTER_0:42
for B being B_Lattice
for a, b being Element of B holds a => b = (a `) "\/" b
proof
let B be B_Lattice; ::_thesis: for a, b being Element of B holds a => b = (a `) "\/" b
let a, b be Element of B; ::_thesis: a => b = (a `) "\/" b
 ( a "/\" ((a `) "\/" b) [= b & ( for c being Element of B st a "/\" c [= b holds
c [= (a `) "\/" b ) ) by Th27;
hence  a => b = (a `) "\/" b by Def7; ::_thesis: verum
end;

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 )
proof
let B be B_Lattice; ::_thesis: for a, b being Element of B holds
( a [= b iff a "/\" (b `) = Bottom B )
let a, b be Element of B; ::_thesis: ( a [= b iff a "/\" (b `) = Bottom B )
reconsider B9 = B as 0_Lattice ;
reconsider B99 = B as 1_Lattice ;
reconsider D = B as D_Lattice ;
reconsider a9 = a, b9 = b, c9 = a "/\" (b `) as Element of B9 ;
reconsider a99 = a, b99 = b as Element of B99 ;
reconsider a1 = a, b1 = b as Element of D ;
thus  ( a [= b implies a "/\" (b `) = Bottom B ) ::_thesis: ( a "/\" (b `) = Bottom B implies a [= b )
proof
assume  a [= b ; ::_thesis: a "/\" (b `) = Bottom B
then  a = a "/\" b by LATTICES:4;
hence a "/\" (b `) = a "/\" (b "/\" (b `)) by LATTICES:def_7
.= a9 "/\" (Bottom B9) by LATTICES:20
.= Bottom B ;
::_thesis: verum
end;
assume  a "/\" (b `) = Bottom B ; ::_thesis: a [= b
then b = b9 "\/" c9 by LATTICES:14
.= (b1 "\/" a1) "/\" (b1 "\/" (b1 `)) by LATTICES:11
.= (b99 "\/" a99) "/\" (Top B99) by LATTICES:21
.= a "\/" b ;
hence  a [= b by LATTICES:def_3; ::_thesis: verum
end;

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 & ( for a being Element of B holds
( a in FB or a ` in FB ) ) ) )
proof
let B be B_Lattice; ::_thesis: for FB being Filter of B holds
( FB is being_ultrafilter iff ( FB <> the carrier of B & ( for a being Element of B holds
( a in FB or a ` in FB ) ) ) )
let FB be Filter of B; ::_thesis: ( FB is being_ultrafilter iff ( FB <> the carrier of B & ( for a being Element of B holds
( a in FB or a ` in FB ) ) ) )
thus  ( FB is being_ultrafilter implies ( FB <> the carrier of B & ( for a being Element of B holds
( a in FB or a ` in FB ) ) ) ) ::_thesis: ( FB <> the carrier of B & ( for a being Element of B holds
( a in FB or a ` in FB ) ) implies FB is being_ultrafilter )
proof
reconsider I = B as I_Lattice ;
assume that
A1: FB <> the carrier of B and
A2: for HB being Filter of B st FB c= HB & HB <> the carrier of B holds
FB = HB ; :: according to FILTER_0:def_3 ::_thesis: ( FB <> the carrier of B & ( for a being Element of B holds
( a in FB or a ` in FB ) ) )
thus  FB <> the carrier of B by A1; ::_thesis: for a being Element of B holds
( a in FB or a ` in FB )
let a be Element of B; ::_thesis: ( a in FB or a ` in FB )
assume A3: not a in FB ; ::_thesis: a ` in FB
A4: a in <.a.) ;
A5: FB \/ <.a.) c= <.(FB \/ <.a.)).) by Def4;
 <.a.) c= FB \/ <.a.) by XBOOLE_1:7;
then  <.a.) c= <.(FB \/ <.a.)).) by A5, XBOOLE_1:1;
then  ( FB c= FB \/ <.a.) & FB <> <.(FB \/ <.a.)).) ) by A3, A4, XBOOLE_1:7;
then  <.(FB \/ <.a.)).) = the carrier of B by A2, A5, XBOOLE_1:1;
then A6: a ` in <.(FB \/ <.a.)).) ;
reconsider a9 = a as Element of I ;
reconsider FI = FB as Filter of I ;
A7: a => (a `) = (a `) "\/" (a `) by Th42;
 <.{a}.) = <.a.) by Th24;
then A8: a9 ` in <.(FI \/ {a9}).) by A6, Th34;
 FB = <.FB.) by Th21;
then  a => (a `) in FB by A8, Th40;
hence  a ` in FB by A7; ::_thesis: verum
end;
assume that
A9: FB <> the carrier of B and
A10: for a being Element of B holds
( a in FB or a ` in FB ) ; ::_thesis: FB is being_ultrafilter
thus  FB <> the carrier of B by A9; :: according to FILTER_0:def_3 ::_thesis: for H being Filter of B st FB c= H & H <> the carrier of B holds
FB = H
let HB be Filter of B; ::_thesis: ( FB c= HB & HB <> the carrier of B implies FB = HB )
assume that
A11: FB c= HB and
A12: HB <> the carrier of B and
A13: FB <> HB ; ::_thesis: contradiction
 not for x being set holds
( x in FB iff x in HB ) by A13, TARSKI:1;
then consider x being set  such that
A14: x in HB and
A15: not x in FB by A11;
reconsider x = x as Element of HB by A14;
 x ` in FB by A10, A15;
then  (x `) "/\" x in HB by A11, Th8;
then A16: Bottom B in HB by LATTICES:20;
 HB = <.HB.) by Th21;
hence  contradiction by A12, A16, Th25; ::_thesis: verum
end;

theorem :: FILTER_0:45
for B being B_Lattice
for FB being Filter of B holds
( ( FB <> <.B.) & FB is prime ) iff FB is being_ultrafilter )
proof
let B be B_Lattice; ::_thesis: for FB being Filter of B holds
( ( FB <> <.B.) & FB is prime ) iff FB is being_ultrafilter )
let FB be Filter of B; ::_thesis: ( ( FB <> <.B.) & FB is prime ) iff FB is being_ultrafilter )
thus  ( FB <> <.B.) & FB is prime implies FB is being_ultrafilter ) ::_thesis: ( FB is being_ultrafilter implies ( FB <> <.B.) & FB is prime ) )
proof
assume that
A1: FB <> <.B.) and
A2: for a, b being Element of B holds
( a "\/" b in FB iff ( a in FB or b in FB ) ) ; :: according to FILTER_0:def_5 ::_thesis: FB is being_ultrafilter
now__::_thesis:_for_a_being_Element_of_B_st_not_a_in_FB_holds_
a_`_in_FB
let a be Element of B; ::_thesis: ( not a in FB implies a ` in FB )
assume A3: not a in FB ; ::_thesis: a ` in FB
 a "\/" (a `) = Top B by LATTICES:21;
then  a "\/" (a `) in FB by Th11;
hence  a ` in FB by A2, A3; ::_thesis: verum
end;
hence  FB is being_ultrafilter by A1, Th44; ::_thesis: verum
end;
assume A4: FB is being_ultrafilter ; ::_thesis: ( FB <> <.B.) & FB is prime )
hence  FB <> <.B.) by Th44; ::_thesis: FB is prime
let a be Element of B; :: according to FILTER_0:def_5 ::_thesis: for q being Element of B holds
( a "\/" q in FB iff ( a in FB or q in FB ) )
let b be Element of B; ::_thesis: ( a "\/" b in FB iff ( a in FB or b in FB ) )
A5: FB <> the carrier of B by A4, Th44;
thus  ( not a "\/" b in FB or a in FB or b in FB ) ::_thesis: ( ( a in FB or b in FB ) implies a "\/" b in FB )
proof
assume that
A6: a "\/" b in FB and
A7: ( not a in FB & not b in FB ) ; ::_thesis: contradiction
 ( a ` in FB & b ` in FB ) by A4, A7, Th44;
then  (a `) "/\" (b `) in FB by Th8;
then  (a "\/" b) ` in FB by LATTICES:24;
then  (a "\/" b) "/\" ((a "\/" b) `) in FB by A6, Th8;
then A8: Bottom B in FB by LATTICES:20;
 FB = <.FB.) by Th21;
hence  contradiction by A5, A8, Th25; ::_thesis: verum
end;
thus  ( ( a in FB or b in FB ) implies a "\/" b in FB ) by Th10; ::_thesis: verum
end;

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 )
proof
let B be B_Lattice; ::_thesis: 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 )
let FB be Filter of B; ::_thesis: ( FB is being_ultrafilter implies for a being Element of B holds
( a in FB iff not a ` in FB ) )
assume A1: FB is being_ultrafilter ; ::_thesis: for a being Element of B holds
( a in FB iff not a ` in FB )
let a be Element of B; ::_thesis: ( a in FB iff not a ` in FB )
thus  ( a in FB implies not a ` in FB ) ::_thesis: ( not a ` in FB implies a in FB )
proof
assume  ( a in FB & a ` in FB ) ; ::_thesis: contradiction
then  a "/\" (a `) in FB by Th8;
then  Bottom B in FB by LATTICES:20;
then  FB = the carrier of B by Th26;
hence  contradiction by A1, Def3; ::_thesis: verum
end;
thus  ( not a ` in FB implies a in FB ) by A1, Th44; ::_thesis: verum
end;

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 & ( ( a in FB & not b in FB ) or ( not a in FB & b in FB ) ) )
proof
let B be B_Lattice; ::_thesis: for a, b being Element of B st a <> b holds
ex FB being Filter of B st
( FB is being_ultrafilter & ( ( a in FB & not b in FB ) or ( not a in FB & b in FB ) ) )
let a, b be Element of B; ::_thesis: ( a <> b implies ex FB being Filter of B st
( FB is being_ultrafilter & ( ( a in FB & not b in FB ) or ( not a in FB & b in FB ) ) ) )
assume  a <> b ; ::_thesis: ex FB being Filter of B st
( FB is being_ultrafilter & ( ( a in FB & not b in FB ) or ( not a in FB & b in FB ) ) )
then  ( not a [= b or not b [= a ) by LATTICES:8;
then  ( a "/\" (b `) <> Bottom B or b "/\" (a `) <> Bottom B ) by Th43;
then  ( ex FB being Filter of B st
( a "/\" (b `) in FB & FB is being_ultrafilter ) or ex FB being Filter of B st
( b "/\" (a `) in FB & FB is being_ultrafilter ) ) by Th20;
then consider FB being Filter of B such that
A1: FB is being_ultrafilter and
A2: ( a "/\" (b `) in FB or b "/\" (a `) in FB ) ;
take  FB ; ::_thesis: ( FB is being_ultrafilter & ( ( a in FB & not b in FB ) or ( not a in FB & b in FB ) ) )
thus  FB is being_ultrafilter by A1; ::_thesis: ( ( a in FB & not b in FB ) or ( not a in FB & b in FB ) )
 ( ( a in FB & b ` in FB ) or ( b in FB & a ` in FB ) ) by A2, Th8;
hence  ( ( a in FB & not b in FB ) or ( not a in FB & b in FB ) ) by A1, Th46; ::_thesis: verum
end;


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 & o2 = the L_meet of L || F & 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 & o2 = the L_meet of L || F & b1 = LattStr(# F,o1,o2 #) ) & ex o1, o2 being BinOp of F st
( o1 = the L_join of L || F & o2 = the L_meet of L || F & 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 & o2 = the L_meet of L || F & b1 = LattStr(# F,o1,o2 #) )
proof
reconsider o1 = the L_join of L || F, o2 = the L_meet of L || F as Function of [:F,F:], the carrier of L by FUNCT_2:32;
A1: dom o1 = [:F,F:] by FUNCT_2:def_1;
 rng o1 c= F
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng o1 or y in F )
assume  y in rng o1 ; ::_thesis: y in F
then consider x being set  such that
A2: x in dom o1 and
A3: y = o1 . x by FUNCT_1:def_3;
reconsider p = x `1 , q = x `2 as Element of F by A2, MCART_1:10;
 x = [(x `1),(x `2)] by A2, MCART_1:21;
then  o1 . x = p "\/" q by A2, FUNCT_1:47;
hence  y in F by A3, Th10; ::_thesis: verum
end;
then reconsider o1 = o1 as Function of [:F,F:],F by A1, FUNCT_2:def_1, RELSET_1:4;
A4: dom o2 = [:F,F:] by FUNCT_2:def_1;
 rng o2 c= F
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng o2 or y in F )
assume  y in rng o2 ; ::_thesis: y in F
then consider x being set  such that
A5: x in dom o2 and
A6: y = o2 . x by FUNCT_1:def_3;
reconsider p = x `1 , q = x `2 as Element of F by A5, MCART_1:10;
 x = [(x `1),(x `2)] by A5, MCART_1:21;
then  o2 . x = p "/\" q by A5, FUNCT_1:47;
hence  y in F by A6, Th8; ::_thesis: verum
end;
then reconsider o2 = o2 as Function of [:F,F:],F by A4, FUNCT_2:def_1, RELSET_1:4;
reconsider K = LattStr(# F,o1,o2 #) as non empty LattStr ;
A7: for a, b being Element of K holds
( the L_join of K . (a,b) = the L_join of L . (a,b) & the L_meet of K . (a,b) = the L_meet of L . (a,b) )
proof
let a, b be Element of K; ::_thesis: ( the L_join of K . (a,b) = the L_join of L . (a,b) & the L_meet of K . (a,b) = the L_meet of L . (a,b) )
 the L_join of K . (a,b) = the L_join of K . [a,b] ;
hence  ( the L_join of K . (a,b) = the L_join of L . (a,b) & the L_meet of K . (a,b) = the L_meet of L . (a,b) ) by A1, A4, FUNCT_1:47; ::_thesis: verum
end;
A8: for a, b, c being Element of K holds a "/\" (b "/\" c) = (a "/\" b) "/\" c
proof
let a, b, c be Element of K; ::_thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c
reconsider a9 = a, b9 = b, c9 = c as Element of F ;
thus a "/\" (b "/\" c) = the L_meet of L . (a,(b "/\" c)) by A7
.= a9 "/\" (b9 "/\" c9) by A7
.= (a9 "/\" b9) "/\" c9 by LATTICES:def_7
.= the L_meet of L . ((a "/\" b),c) by A7
.= (a "/\" b) "/\" c by A7 ; ::_thesis: verum
end;
A9: for a, b being Element of K holds a "/\" (a "\/" b) = a
proof
let a, b be Element of K; ::_thesis: a "/\" (a "\/" b) = a
reconsider a9 = a, b9 = b as Element of F ;
thus a "/\" (a "\/" b) = the L_meet of L . (a,(a "\/" b)) by A7
.= a9 "/\" (a9 "\/" b9) by A7
.= a by LATTICES:def_9 ; ::_thesis: verum
end;
A10: for a, b being Element of K holds a "/\" b = b "/\" a
proof
let a, b be Element of K; ::_thesis: a "/\" b = b "/\" a
reconsider a9 = a, b9 = b as Element of F ;
thus a "/\" b = the L_meet of L . (a9,b9) by A7
.= b9 "/\" a9 by LATTICES:def_2
.= b "/\" a by A7 ; ::_thesis: verum
end;
A11: for a, b being Element of K holds (a "/\" b) "\/" b = b
proof
let a, b be Element of K; ::_thesis: (a "/\" b) "\/" b = b
reconsider a9 = a, b9 = b as Element of F ;
thus (a "/\" b) "\/" b = the L_join of L . ((a "/\" b),b) by A7
.= (a9 "/\" b9) "\/" b9 by A7
.= b by LATTICES:def_8 ; ::_thesis: verum
end;
A12: for a, b being Element of K holds a "\/" b = b "\/" a
proof
let a, b be Element of K; ::_thesis: a "\/" b = b "\/" a
reconsider a9 = a, b9 = b as Element of F ;
thus a "\/" b = the L_join of L . (a9,b9) by A7
.= b9 "\/" a9 by LATTICES:def_1
.= b "\/" a by A7 ; ::_thesis: verum
end;
 for a, b, c being Element of K holds a "\/" (b "\/" c) = (a "\/" b) "\/" c
proof
let a, b, c be Element of K; ::_thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c
reconsider a9 = a, b9 = b, c9 = c as Element of F ;
thus a "\/" (b "\/" c) = the L_join of L . (a,(b "\/" c)) by A7
.= a9 "\/" (b9 "\/" c9) by A7
.= (a9 "\/" b9) "\/" c9 by LATTICES:def_5
.= the L_join of L . ((a "\/" b),c) by A7
.= (a "\/" b) "\/" c by A7 ; ::_thesis: verum
end;
then  ( K is join-commutative & K is join-associative & K is meet-absorbing & K is meet-commutative & K is meet-associative & K is join-absorbing ) by A12, A11, A10, A8, A9, LATTICES:def_4, LATTICES:def_5, LATTICES:def_6, LATTICES:def_7, LATTICES:def_8, LATTICES:def_9;
then reconsider Q = K as Lattice ;
take  Q ; ::_thesis: ex o1, o2 being BinOp of F st
( o1 = the L_join of L || F & o2 = the L_meet of L || F & Q = LattStr(# F,o1,o2 #) )
take  o1 ; ::_thesis: ex o2 being BinOp of F st
( o1 = the L_join of L || F & o2 = the L_meet of L || F & Q = LattStr(# F,o1,o2 #) )
take  o2 ; ::_thesis: ( o1 = the L_join of L || F & o2 = the L_meet of L || F & Q = LattStr(# F,o1,o2 #) )
thus  ( o1 = the L_join of L || F & o2 = the L_meet of L || F & Q = LattStr(# F,o1,o2 #) ) ; ::_thesis: verum
end;
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 & o2 = the L_meet of L || F & 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
proof
 ex o1, o2 being BinOp of F st
( o1 = the L_join of L || F & o2 = the L_meet of L || F & latt F = LattStr(# F,o1,o2 #) ) by Def9;
hence  latt F is strict ; ::_thesis: verum
end;
end;

theorem :: FILTER_0:48
for L being strict Lattice holds latt <.L.) = L
proof
let L be strict Lattice; ::_thesis: latt <.L.) = L
 dom the L_meet of L = [: the carrier of L, the carrier of L:] by FUNCT_2:def_1;
then A1: the L_meet of L = the L_meet of L || the carrier of L by RELAT_1:68;
 dom the L_join of L = [: the carrier of L, the carrier of L:] by FUNCT_2:def_1;
then  the L_join of L = the L_join of L || the carrier of L by RELAT_1:68;
hence  latt <.L.) = L by A1, Def9; ::_thesis: verum
end;

theorem Th49: :: FILTER_0:49
for L being Lattice
for F being Filter of L holds
( the carrier of (latt F) = F & the L_join of (latt F) = the L_join of L || F & the L_meet of (latt F) = the L_meet of L || F )
proof
let L be Lattice; ::_thesis: for F being Filter of L holds
( the carrier of (latt F) = F & the L_join of (latt F) = the L_join of L || F & the L_meet of (latt F) = the L_meet of L || F )
let F be Filter of L; ::_thesis: ( the carrier of (latt F) = F & the L_join of (latt F) = the L_join of L || F & the L_meet of (latt F) = the L_meet of L || F )
 ex o1, o2 being BinOp of F st
( o1 = the L_join of L || F & o2 = the L_meet of L || F & latt F = LattStr(# F,o1,o2 #) ) by Def9;
hence  ( the carrier of (latt F) = F & the L_join of (latt F) = the L_join of L || F & the L_meet of (latt F) = the L_meet of L || F ) ; ::_thesis: verum
end;

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 & q = q9 holds
( p "\/" q = p9 "\/" q9 & p "/\" q = p9 "/\" q9 )
proof
let L be Lattice; ::_thesis: for p, q being Element of L
for F being Filter of L
for p9, q9 being Element of (latt F) st p = p9 & q = q9 holds
( p "\/" q = p9 "\/" q9 & p "/\" q = p9 "/\" q9 )
let p, q be Element of L; ::_thesis: for F being Filter of L
for p9, q9 being Element of (latt F) st p = p9 & q = q9 holds
( p "\/" q = p9 "\/" q9 & p "/\" q = p9 "/\" q9 )
let F be Filter of L; ::_thesis: for p9, q9 being Element of (latt F) st p = p9 & q = q9 holds
( p "\/" q = p9 "\/" q9 & p "/\" q = p9 "/\" q9 )
let p9, q9 be Element of (latt F); ::_thesis: ( p = p9 & q = q9 implies ( p "\/" q = p9 "\/" q9 & p "/\" q = p9 "/\" q9 ) )
assume A1: ( p = p9 & q = q9 ) ; ::_thesis: ( p "\/" q = p9 "\/" q9 & p "/\" q = p9 "/\" q9 )
consider o1, o2 being BinOp of F such that
A2: o1 = the L_join of L || F and
A3: o2 = the L_meet of L || F and
A4: latt F = LattStr(# F,o1,o2 #) by Def9;
 dom o1 = [:F,F:] by FUNCT_2:def_1;
then  [p,q] in dom o1 by A1, A4, ZFMISC_1:87;
hence  p "\/" q = p9 "\/" q9 by A1, A2, A4, FUNCT_1:47; ::_thesis: p "/\" q = p9 "/\" q9
 dom o2 = [:F,F:] by FUNCT_2:def_1;
then  [p,q] in dom o2 by A1, A4, ZFMISC_1:87;
hence  p "/\" q = p9 "/\" q9 by A1, A3, A4, FUNCT_1:47; ::_thesis: verum
end;

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 & q = q9 holds
( p [= q iff p9 [= q9 )
proof
let L be Lattice; ::_thesis: for p, q being Element of L
for F being Filter of L
for p9, q9 being Element of (latt F) st p = p9 & q = q9 holds
( p [= q iff p9 [= q9 )
let p, q be Element of L; ::_thesis: for F being Filter of L
for p9, q9 being Element of (latt F) st p = p9 & q = q9 holds
( p [= q iff p9 [= q9 )
let F be Filter of L; ::_thesis: for p9, q9 being Element of (latt F) st p = p9 & q = q9 holds
( p [= q iff p9 [= q9 )
let p9, q9 be Element of (latt F); ::_thesis: ( p = p9 & q = q9 implies ( p [= q iff p9 [= q9 ) )
A1: ( p [= q iff p "\/" q = q ) by LATTICES:def_3;
A2: ( p9 [= q9 iff p9 "\/" q9 = q9 ) by LATTICES:def_3;
assume  ( p = p9 & q = q9 ) ; ::_thesis: ( p [= q iff p9 [= q9 )
hence  ( p [= q iff p9 [= q9 ) by A1, A2, Th50; ::_thesis: verum
end;

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
proof
let L be Lattice; ::_thesis: for F being Filter of L st L is upper-bounded holds
latt F is upper-bounded
let F be Filter of L; ::_thesis: ( L is upper-bounded implies latt F is upper-bounded )
given p being Element of L such that A1: for q being Element of L holds
( p "\/" q = p & q "\/" p = p ) ; :: according to LATTICES:def_14 ::_thesis: latt F is upper-bounded
consider q being Element of L such that
A2: q in F by SUBSET_1:4;
A3: ex o1, o2 being BinOp of F st
( o1 = the L_join of L || F & o2 = the L_meet of L || F & latt F = LattStr(# F,o1,o2 #) ) by Def9;
 p "\/" q = p by A1;
then reconsider p9 = p as Element of (latt F) by A2, A3, Th10;
take  p9 ; :: according to LATTICES:def_14 ::_thesis: for b1 being Element of the carrier of (latt F) holds
( p9 "\/" b1 = p9 & b1 "\/" p9 = p9 )
let r be Element of (latt F); ::_thesis: ( p9 "\/" r = p9 & r "\/" p9 = p9 )
reconsider r9 = r as Element of F by A3;
thus p9 "\/" r = p "\/" r9 by Th50
.= p9 by A1 ; ::_thesis: r "\/" p9 = p9
hence  r "\/" p9 = p9 ; ::_thesis: verum
end;

theorem :: FILTER_0:53
for L being Lattice
for F being Filter of L st L is modular holds
latt F is modular
proof
let L be Lattice; ::_thesis: for F being Filter of L st L is modular holds
latt F is modular
let F be Filter of L; ::_thesis: ( L is modular implies latt F is modular )
assume A1: for a, b, c being Element of L st a [= c holds
a "\/" (b "/\" c) = (a "\/" b) "/\" c ; :: according to LATTICES:def_12 ::_thesis: latt F is modular
let a, b, c be Element of (latt F); :: according to LATTICES:def_12 ::_thesis: ( not a [= c or a "\/" (b "/\" c) = (a "\/" b) "/\" c )
assume A2: a [= c ; ::_thesis: a "\/" (b "/\" c) = (a "\/" b) "/\" c
reconsider p = a, q = b, r = c as Element of F by Th49;
 b "/\" c = q "/\" r by Th50;
then A3: a "\/" (b "/\" c) = p "\/" (q "/\" r) by Th50;
 a "\/" b = p "\/" q by Th50;
then A4: (a "\/" b) "/\" c = (p "\/" q) "/\" r by Th50;
 p [= r by A2, Th51;
hence  a "\/" (b "/\" c) = (a "\/" b) "/\" c by A1, A3, A4; ::_thesis: verum
end;

theorem Th54: :: FILTER_0:54
for L being Lattice
for F being Filter of L st L is distributive holds
latt F is distributive
proof
let L be Lattice; ::_thesis: for F being Filter of L st L is distributive holds
latt F is distributive
let F be Filter of L; ::_thesis: ( L is distributive implies latt F is distributive )
assume A1: for p, q, r being Element of L holds p "/\" (q "\/" r) = (p "/\" q) "\/" (p "/\" r) ; :: according to LATTICES:def_11 ::_thesis: latt F is distributive
let p9, q9, r9 be Element of (latt F); :: according to LATTICES:def_11 ::_thesis: p9 "/\" (q9 "\/" r9) = (p9 "/\" q9) "\/" (p9 "/\" r9)
reconsider p = p9, q = q9, r = r9, qr = q9 "\/" r9 as Element of F by Th49;
A2: ( p9 "/\" q9 = p "/\" q & p9 "/\" r9 = p "/\" r ) by Th50;
thus p9 "/\" (q9 "\/" r9) = p "/\" qr by Th50
.= p "/\" (q "\/" r) by Th50
.= (p "/\" q) "\/" (p "/\" r) by A1
.= (p9 "/\" q9) "\/" (p9 "/\" r9) by A2, Th50 ; ::_thesis: verum
end;

theorem :: FILTER_0:55
for L being Lattice
for F being Filter of L st L is I_Lattice holds
latt F is implicative
proof
let L be Lattice; ::_thesis: for F being Filter of L st L is I_Lattice holds
latt F is implicative
let F be Filter of L; ::_thesis: ( L is I_Lattice implies latt F is implicative )
assume A1: L is I_Lattice ; ::_thesis: latt F is implicative
then reconsider I = L as I_Lattice ;
reconsider FI = F as Filter of I ;
let p9, q9 be Element of (latt F); :: according to FILTER_0:def_6 ::_thesis: ex r being Element of (latt F) st
( p9 "/\" r [= q9 & ( for r1 being Element of (latt F) st p9 "/\" r1 [= q9 holds
r1 [= r ) )
reconsider p = p9, q = q9 as Element of F by Th49;
consider r being Element of L such that
A2: p "/\" r [= q and
A3: for r1 being Element of L st p "/\" r1 [= q holds
r1 [= r by A1, Def6;
reconsider i = p, j = q as Element of I ;
A4: i => j in FI by Th30;
 i => j = r by A2, A3, Def7;
then reconsider r9 = r as Element of (latt F) by A4, Th49;
take  r9 ; ::_thesis: ( p9 "/\" r9 [= q9 & ( for r1 being Element of (latt F) st p9 "/\" r1 [= q9 holds
r1 [= r9 ) )
 p "/\" r = p9 "/\" r9 by Th50;
hence  p9 "/\" r9 [= q9 by A2, Th51; ::_thesis: for r1 being Element of (latt F) st p9 "/\" r1 [= q9 holds
r1 [= r9
let s9 be Element of (latt F); ::_thesis: ( p9 "/\" s9 [= q9 implies s9 [= r9 )
assume A5: p9 "/\" s9 [= q9 ; ::_thesis: s9 [= r9
reconsider s = s9 as Element of F by Th49;
 p "/\" s = p9 "/\" s9 by Th50;
then  p "/\" s [= q by A5, Th51;
then  s [= r by A3;
hence  s9 [= r9 by Th51; ::_thesis: verum
end;

registration
let L be Lattice;
let p be Element of L;
cluster latt <.p.) ->  lower-bounded ;
coherence
 latt <.p.) is lower-bounded
proof
 the carrier of (latt <.p.)) = <.p.) by Th49;
then reconsider p9 = p as Element of (latt <.p.)) by Th16;
take  p9 ; :: according to LATTICES:def_13 ::_thesis: for b1 being Element of the carrier of (latt <.p.)) holds
( p9 "/\" b1 = p9 & b1 "/\" p9 = p9 )
let q9 be Element of (latt <.p.)); ::_thesis: ( p9 "/\" q9 = p9 & q9 "/\" p9 = p9 )
reconsider q = q9 as Element of <.p.) by Th49;
 p [= q by Th15;
then  p "/\" q = p by LATTICES:4;
hence  ( p9 "/\" q9 = p9 & q9 "/\" p9 = p9 ) by Th50; ::_thesis: verum
end;
end;

theorem Th56: :: FILTER_0:56
for L being Lattice
for p being Element of L holds Bottom (latt <.p.)) = p
proof
let L be Lattice; ::_thesis: for p being Element of L holds Bottom (latt <.p.)) = p
let p be Element of L; ::_thesis: Bottom (latt <.p.)) = p
consider q9 being Element of (latt <.p.)) such that
A1: for r9 being Element of (latt <.p.)) holds
( q9 "/\" r9 = q9 & r9 "/\" q9 = q9 ) by LATTICES:def_13;
 the carrier of (latt <.p.)) = <.p.) by Th49;
then reconsider p9 = p as Element of (latt <.p.)) by Th16;
reconsider q = q9 as Element of <.p.) by Th49;
 q9 "/\" p9 = q9 by A1;
then  q9 [= p9 by LATTICES:4;
then A2: q [= p by Th51;
A3: p [= q by Th15;
 q9 = Bottom (latt <.p.)) by A1, RLSUB_2:64;
hence  Bottom (latt <.p.)) = p by A2, A3, LATTICES:8; ::_thesis: verum
end;

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
proof
let L be Lattice; ::_thesis: for p being Element of L st L is upper-bounded holds
Top (latt <.p.)) = Top L
let p be Element of L; ::_thesis: ( L is upper-bounded implies Top (latt <.p.)) = Top L )
given q being Element of L such that A1: for r being Element of L holds
( q "\/" r = q & r "\/" q = q ) ; :: according to LATTICES:def_14 ::_thesis: Top (latt <.p.)) = Top L
 L is 1_Lattice by A1, LATTICES:def_14;
then  Top L in <.p.) by Th11;
then reconsider q9 = Top L as Element of (latt <.p.)) by Th49;
A2: q = Top L by A1, RLSUB_2:65;
now__::_thesis:_for_r9_being_Element_of_(latt_<.p.))_holds_r9_"\/"_q9_=_q9
let r9 be Element of (latt <.p.)); ::_thesis: r9 "\/" q9 = q9
reconsider r = r9 as Element of <.p.) by Th49;
thus r9 "\/" q9 = q "\/" r by A2, Th50
.= q9 by A1, A2 ; ::_thesis: verum
end;
hence  Top (latt <.p.)) = Top L by RLSUB_2:65; ::_thesis: verum
end;

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
proof
let L be Lattice; ::_thesis: for p being Element of L st L is 1_Lattice holds
latt <.p.) is bounded
let p be Element of L; ::_thesis: ( L is 1_Lattice implies latt <.p.) is bounded )
assume  L is 1_Lattice ; ::_thesis: latt <.p.) is bounded
hence  ( latt <.p.) is lower-bounded & latt <.p.) is upper-bounded ) by Th52; :: according to LATTICES:def_15 ::_thesis: verum
end;

theorem Th59: :: FILTER_0:59
for L being Lattice
for p being Element of L st L is C_Lattice & L is M_Lattice holds
latt <.p.) is C_Lattice
proof
let L be Lattice; ::_thesis: for p being Element of L st L is C_Lattice & L is M_Lattice holds
latt <.p.) is C_Lattice
let p be Element of L; ::_thesis: ( L is C_Lattice & L is M_Lattice implies latt <.p.) is C_Lattice )
assume that
A1: L is C_Lattice and
A2: L is M_Lattice ; ::_thesis: latt <.p.) is C_Lattice
reconsider B = L as C_Lattice by A1;
reconsider M = latt <.p.) as 01_Lattice by A1, Th58;
 M is complemented
proof
let r9 be Element of M; :: according to LATTICES:def_19 ::_thesis: ex b1 being Element of the carrier of M st b1 is_a_complement_of r9
reconsider r = r9 as Element of <.p.) by Th49;
reconsider p1 = p as Element of B ;
consider q being Element of L such that
A3: q is_a_complement_of r by A1, LATTICES:def_19;
 the carrier of (latt <.p.)) = <.p.) by Th49;
then reconsider q9 = p "\/" q as Element of M by Th16;
take  q9 ; ::_thesis: q9 is_a_complement_of r9
thus q9 "\/" r9 = (p "\/" q) "\/" r by Th50
.= p "\/" (q "\/" r) by LATTICES:def_5
.= p1 "\/" (Top B) by A3, LATTICES:def_18
.= Top L
.= Top M by A1, Th57 ; :: according to LATTICES:def_18 ::_thesis: ( r9 "\/" q9 = Top M & q9 "/\" r9 = Bottom M & r9 "/\" q9 = Bottom M )
hence  r9 "\/" q9 = Top M ; ::_thesis: ( q9 "/\" r9 = Bottom M & r9 "/\" q9 = Bottom M )
 p [= r by Th15;
then  (p "\/" q) "/\" r = p "\/" (q "/\" r) by A2, LATTICES:def_12;
hence q9 "/\" r9 = p "\/" (q "/\" r) by Th50
.= p1 "\/" (Bottom B) by A3, LATTICES:def_18
.= p
.= Bottom M by Th56 ;
::_thesis: r9 "/\" q9 = Bottom M
hence  r9 "/\" q9 = Bottom M ; ::_thesis: verum
end;
hence  latt <.p.) is C_Lattice ; ::_thesis: verum
end;

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
proof
let L be Lattice; ::_thesis: for p being Element of L st L is B_Lattice holds
latt <.p.) is B_Lattice
let p be Element of L; ::_thesis: ( L is B_Lattice implies latt <.p.) is B_Lattice )
assume  L is B_Lattice ; ::_thesis: latt <.p.) is B_Lattice
then  latt <.p.) is distributive bounded complemented Lattice by Th54, Th59;
hence  latt <.p.) is B_Lattice ; ::_thesis: verum
end;

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 & j <=> k in FI holds
i <=> k in FI
proof
let I be I_Lattice; ::_thesis: for i, j, k being Element of I
for FI being Filter of I st i <=> j in FI & j <=> k in FI holds
i <=> k in FI
let i, j, k be Element of I; ::_thesis: for FI being Filter of I st i <=> j in FI & j <=> k in FI holds
i <=> k in FI
let FI be Filter of I; ::_thesis: ( i <=> j in FI & j <=> k in FI implies i <=> k in FI )
assume A1: ( i <=> j in FI & j <=> k in FI ) ; ::_thesis: i <=> k in FI
then  ( j => i in FI & k => j in FI ) by Th8;
then A2: k => i in FI by Th41;
 ( i => j in FI & j => k in FI ) by A1, Th8;
then  i => k in FI by Th41;
hence  i <=> k in FI by A2, Th8; ::_thesis: verum
end;

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 & ( 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 & ( for p, q being Element of L holds
( [p,q] in b1 iff p <=> q in F ) ) )
proof
defpred S1[ set , set ] means  ex p, q being Element of L st
( $1 = p & $2 = q & p <=> q in F );
consider R being Relation such that
A1: for x, y being set holds
( [x,y] in R iff ( x in the carrier of L & y in the carrier of L & S1[x,y] ) ) from RELAT_1:sch_1();
take  R ; ::_thesis: ( field R c= the carrier of L & ( for p, q being Element of L holds
( [p,q] in R iff p <=> q in F ) ) )
thus  field R c= the carrier of L ::_thesis: for p, q being Element of L holds
( [p,q] in R iff p <=> q in F )
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in field R or x in the carrier of L )
assume  x in field R ; ::_thesis: x in the carrier of L
then  ex y being set st
( [x,y] in R or [y,x] in R ) by WELLSET1:1;
hence  x in the carrier of L by A1; ::_thesis: verum
end;
let p, q be Element of L; ::_thesis: ( [p,q] in R iff p <=> q in F )
thus  ( [p,q] in R implies p <=> q in F ) ::_thesis: ( p <=> q in F implies [p,q] in R )
proof
assume  [p,q] in R ; ::_thesis: p <=> q in F
then  ex p1, q1 being Element of L st
( p = p1 & q = q1 & p1 <=> q1 in F ) by A1;
hence  p <=> q in F ; ::_thesis: verum
end;
thus  ( p <=> q in F implies [p,q] in R ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Relation st field b1 c= the carrier of L & ( for p, q being Element of L holds
( [p,q] in b1 iff p <=> q in F ) ) & field b2 c= the carrier of L & ( for p, q being Element of L holds
( [p,q] in b2 iff p <=> q in F ) ) holds
b1 = b2
proof
let R1, R2 be Relation; ::_thesis: ( field R1 c= the carrier of L & ( for p, q being Element of L holds
( [p,q] in R1 iff p <=> q in F ) ) & field R2 c= the carrier of L & ( for p, q being Element of L holds
( [p,q] in R2 iff p <=> q in F ) ) implies R1 = R2 )
assume that
A2: field R1 c= the carrier of L and
A3: for p, q being Element of L holds
( [p,q] in R1 iff p <=> q in F ) and
A4: field R2 c= the carrier of L and
A5: for p, q being Element of L holds
( [p,q] in R2 iff p <=> q in F ) ; ::_thesis: R1 = R2
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b1 being set holds
( ( not [x,b1] in R1 or [x,b1] in R2 ) & ( not [x,b1] in R2 or [x,b1] in R1 ) )
let y be set ; ::_thesis: ( ( not [x,y] in R1 or [x,y] in R2 ) & ( not [x,y] in R2 or [x,y] in R1 ) )
thus  ( [x,y] in R1 implies [x,y] in R2 ) ::_thesis: ( not [x,y] in R2 or [x,y] in R1 )
proof
assume A6: [x,y] in R1 ; ::_thesis: [x,y] in R2
then  ( x in field R1 & y in field R1 ) by RELAT_1:15;
then reconsider p = x, q = y as Element of L by A2;
 p <=> q in F by A3, A6;
hence  [x,y] in R2 by A5; ::_thesis: verum
end;
assume A7: [x,y] in R2 ; ::_thesis: [x,y] in R1
then  ( x in field R2 & y in field R2 ) by RELAT_1:15;
then reconsider p = x, q = y as Element of L by A4;
 p <=> q in F by A5, A7;
hence  [x,y] in R1 by A3; ::_thesis: verum
end;
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 & ( 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
proof
let L be Lattice; ::_thesis: for F being Filter of L holds equivalence_wrt F is Relation of the carrier of L
let F be Filter of L; ::_thesis: equivalence_wrt F is Relation of the carrier of L
 equivalence_wrt F c= [: the carrier of L, the carrier of L:]
proof
let y be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds
( not [y,b1] in equivalence_wrt F or [y,b1] in [: the carrier of L, the carrier of L:] )
let z be set ; ::_thesis: ( not [y,z] in equivalence_wrt F or [y,z] in [: the carrier of L, the carrier of L:] )
assume  [y,z] in equivalence_wrt F ; ::_thesis: [y,z] in [: the carrier of L, the carrier of L:]
then A1: ( y in field (equivalence_wrt F) & z in field (equivalence_wrt F) ) by RELAT_1:15;
 field (equivalence_wrt F) c= the carrier of L by Def11;
hence  [y,z] in [: the carrier of L, the carrier of L:] by A1, ZFMISC_1:87; ::_thesis: verum
end;
hence  equivalence_wrt F is Relation of the carrier of L ; ::_thesis: verum
end;

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
proof
let L be Lattice; ::_thesis: for F being Filter of L st L is I_Lattice holds
equivalence_wrt F is_reflexive_in the carrier of L
let F be Filter of L; ::_thesis: ( L is I_Lattice implies equivalence_wrt F is_reflexive_in the carrier of L )
assume A1: L is I_Lattice ; ::_thesis: equivalence_wrt F is_reflexive_in the carrier of L
let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in the carrier of L or [x,x] in equivalence_wrt F )
assume  x in the carrier of L ; ::_thesis: [x,x] in equivalence_wrt F
then reconsider p = x as Element of L ;
 p => p = Top L by A1, Th28;
then  p <=> p = Top L ;
then  p <=> p in F by A1, Th11;
hence  [x,x] in equivalence_wrt F by Def11; ::_thesis: verum
end;

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
proof
let L be Lattice; ::_thesis: for F being Filter of L holds equivalence_wrt F is_symmetric_in the carrier of L
let F be Filter of L; ::_thesis: equivalence_wrt F is_symmetric_in the carrier of L
let x be set ; :: according to RELAT_2:def_3 ::_thesis: for b1 being set holds
( not x in the carrier of L or not b1 in the carrier of L or not [x,b1] in equivalence_wrt F or [b1,x] in equivalence_wrt F )
let y be set ; ::_thesis: ( not x in the carrier of L or not y in the carrier of L or not [x,y] in equivalence_wrt F or [y,x] in equivalence_wrt F )
assume  ( x in the carrier of L & y in the carrier of L ) ; ::_thesis: ( not [x,y] in equivalence_wrt F or [y,x] in equivalence_wrt F )
then reconsider p = x, q = y as Element of L ;
assume  [x,y] in equivalence_wrt F ; ::_thesis: [y,x] in equivalence_wrt F
then  p <=> q in F by Def11;
then  q <=> p in F ;
hence  [y,x] in equivalence_wrt F by Def11; ::_thesis: verum
end;

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
proof
let L be Lattice; ::_thesis: for F being Filter of L st L is I_Lattice holds
equivalence_wrt F is_transitive_in the carrier of L
let F be Filter of L; ::_thesis: ( L is I_Lattice implies equivalence_wrt F is_transitive_in the carrier of L )
assume A1: L is I_Lattice ; ::_thesis: equivalence_wrt F is_transitive_in the carrier of L
let x be set ; :: according to RELAT_2:def_8 ::_thesis: for b1, b2 being set holds
( not x in the carrier of L or not b1 in the carrier of L or not b2 in the carrier of L or not [x,b1] in equivalence_wrt F or not [b1,b2] in equivalence_wrt F or [x,b2] in equivalence_wrt F )
let y, z be set ; ::_thesis: ( not x in the carrier of L or not y in the carrier of L or not z in the carrier of L or not [x,y] in equivalence_wrt F or not [y,z] in equivalence_wrt F or [x,z] in equivalence_wrt F )
assume  ( x in the carrier of L & y in the carrier of L & z in the carrier of L ) ; ::_thesis: ( not [x,y] in equivalence_wrt F or not [y,z] in equivalence_wrt F or [x,z] in equivalence_wrt F )
then reconsider p = x, q = y, r = z as Element of L ;
assume  ( [x,y] in equivalence_wrt F & [y,z] in equivalence_wrt F ) ; ::_thesis: [x,z] in equivalence_wrt F
then  ( p <=> q in F & q <=> r in F ) by Def11;
then  p <=> r in F by A1, Th62;
hence  [x,z] in equivalence_wrt F by Def11; ::_thesis: verum
end;

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
proof
let L be Lattice; ::_thesis: for F being Filter of L st L is I_Lattice holds
equivalence_wrt F is Equivalence_Relation of the carrier of L
let F be Filter of L; ::_thesis: ( L is I_Lattice implies equivalence_wrt F is Equivalence_Relation of the carrier of L )
reconsider R = equivalence_wrt F as Relation of the carrier of L by Th63;
A1: R is_symmetric_in the carrier of L by Th65;
assume A2: L is I_Lattice ; ::_thesis: equivalence_wrt F is Equivalence_Relation of the carrier of L
then  R is_reflexive_in the carrier of L by Th64;
then A3: ( field R = the carrier of L & dom R = the carrier of L ) by ORDERS_1:13;
 R is_transitive_in the carrier of L by A2, Th66;
hence  equivalence_wrt F is Equivalence_Relation of the carrier of L by A3, A1, PARTFUN1:def_2, RELAT_2:def_11, RELAT_2:def_16; ::_thesis: verum
end;

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
proof
let L be Lattice; ::_thesis: for F being Filter of L st L is I_Lattice holds
field (equivalence_wrt F) = the carrier of L
let F be Filter of L; ::_thesis: ( L is I_Lattice implies field (equivalence_wrt F) = the carrier of L )
assume  L is I_Lattice ; ::_thesis: field (equivalence_wrt F) = the carrier of L
then  equivalence_wrt F is Equivalence_Relation of the carrier of L by Th67;
hence  field (equivalence_wrt F) = the carrier of L by ORDERS_1:12; ::_thesis: verum
end;

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 )
proof
let L be Lattice; ::_thesis: 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 )
let p, q be Element of L; ::_thesis: for F being Filter of L holds
( p,q are_equivalence_wrt F iff [p,q] in equivalence_wrt F )
let F be Filter of L; ::_thesis: ( p,q are_equivalence_wrt F iff [p,q] in equivalence_wrt F )
 ( p,q are_equivalence_wrt F iff p <=> q in F ) by Def12;
hence  ( p,q are_equivalence_wrt F iff [p,q] in equivalence_wrt F ) by Def11; ::_thesis: verum
end;

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 & a,a are_equivalence_wrt FB )
proof
let B be B_Lattice; ::_thesis: 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 & a,a are_equivalence_wrt FB )
let FB be Filter of B; ::_thesis: 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 & a,a are_equivalence_wrt FB )
let I be I_Lattice; ::_thesis: 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 & a,a are_equivalence_wrt FB )
let i be Element of I; ::_thesis: for FI being Filter of I
for a being Element of B holds
( i,i are_equivalence_wrt FI & a,a are_equivalence_wrt FB )
let FI be Filter of I; ::_thesis: for a being Element of B holds
( i,i are_equivalence_wrt FI & a,a are_equivalence_wrt FB )
let a be Element of B; ::_thesis: ( i,i are_equivalence_wrt FI & a,a are_equivalence_wrt FB )
A2: a => a = Top B by Th28;
 ( i => i = Top I & (Top I) "/\" (Top I) = Top I ) by Th28;
hence  ( i <=> i in FI & a <=> a in FB ) by A2, Th11; :: according to FILTER_0:def_12 ::_thesis: verum
end;

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
proof
let L be Lattice; ::_thesis: 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
let p, q be Element of L; ::_thesis: for F being Filter of L st p,q are_equivalence_wrt F holds
q,p are_equivalence_wrt F
let F be Filter of L; ::_thesis: ( p,q are_equivalence_wrt F implies q,p are_equivalence_wrt F )
assume  p <=> q in F ; :: according to FILTER_0:def_12 ::_thesis: q,p are_equivalence_wrt F
hence  q <=> p in F ; :: according to FILTER_0:def_12 ::_thesis: verum
end;

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 & j,k are_equivalence_wrt FI implies i,k are_equivalence_wrt FI ) & ( a,b are_equivalence_wrt FB & b,c are_equivalence_wrt FB implies a,c are_equivalence_wrt FB ) )
proof
let B be B_Lattice; ::_thesis: 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 & j,k are_equivalence_wrt FI implies i,k are_equivalence_wrt FI ) & ( a,b are_equivalence_wrt FB & b,c are_equivalence_wrt FB implies a,c are_equivalence_wrt FB ) )
let FB be Filter of B; ::_thesis: 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 & j,k are_equivalence_wrt FI implies i,k are_equivalence_wrt FI ) & ( a,b are_equivalence_wrt FB & b,c are_equivalence_wrt FB implies a,c are_equivalence_wrt FB ) )
let I be I_Lattice; ::_thesis: 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 & j,k are_equivalence_wrt FI implies i,k are_equivalence_wrt FI ) & ( a,b are_equivalence_wrt FB & b,c are_equivalence_wrt FB implies a,c are_equivalence_wrt FB ) )
let i, j, k be Element of I; ::_thesis: for FI being Filter of I
for a, b, c being Element of B holds
( ( i,j are_equivalence_wrt FI & j,k are_equivalence_wrt FI implies i,k are_equivalence_wrt FI ) & ( a,b are_equivalence_wrt FB & b,c are_equivalence_wrt FB implies a,c are_equivalence_wrt FB ) )
let FI be Filter of I; ::_thesis: for a, b, c being Element of B holds
( ( i,j are_equivalence_wrt FI & j,k are_equivalence_wrt FI implies i,k are_equivalence_wrt FI ) & ( a,b are_equivalence_wrt FB & b,c are_equivalence_wrt FB implies a,c are_equivalence_wrt FB ) )
let a, b, c be Element of B; ::_thesis: ( ( i,j are_equivalence_wrt FI & j,k are_equivalence_wrt FI implies i,k are_equivalence_wrt FI ) & ( a,b are_equivalence_wrt FB & b,c are_equivalence_wrt FB implies a,c are_equivalence_wrt FB ) )
thus  ( i,j are_equivalence_wrt FI & j,k are_equivalence_wrt FI implies i,k are_equivalence_wrt FI ) ::_thesis: ( a,b are_equivalence_wrt FB & b,c are_equivalence_wrt FB implies a,c are_equivalence_wrt FB )
proof
assume  ( i <=> j in FI & j <=> k in FI ) ; :: according to FILTER_0:def_12 ::_thesis: i,k are_equivalence_wrt FI
hence  i <=> k in FI by Th62; :: according to FILTER_0:def_12 ::_thesis: verum
end;
assume  ( a <=> b in FB & b <=> c in FB ) ; :: according to FILTER_0:def_12 ::_thesis: a,c are_equivalence_wrt FB
hence  a <=> c in FB by Th62; :: according to FILTER_0:def_12 ::_thesis: verum
end;

begin

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 & z [= y & ( for z9 being Element of L st z9 [= x & z9 [= y holds
z9 [= z ) holds
z = x "/\" y
proof
let L be non empty join-commutative meet-commutative meet-associative meet-absorbing join-absorbing LattStr ; ::_thesis: for x, y, z being Element of L st z [= x & z [= y & ( for z9 being Element of L st z9 [= x & z9 [= y holds
z9 [= z ) holds
z = x "/\" y
let x, y, z be Element of L; ::_thesis: ( z [= x & z [= y & ( for z9 being Element of L st z9 [= x & z9 [= y holds
z9 [= z ) implies z = x "/\" y )
assume that
A1: ( z [= x & z [= y ) and
A2: for z9 being Element of L st z9 [= x & z9 [= y holds
z9 [= z ; ::_thesis: z = x "/\" y
 ( x "/\" y [= x & x "/\" y [= y ) by LATTICES:6;
then A3: x "/\" y [= z by A2;
 z [= x "/\" y by A1, Th7;
hence  z = x "/\" y by A3, LATTICES:8; ::_thesis: verum
end;

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 & y [= z & ( for z9 being Element of L st x [= z9 & y [= z9 holds
z [= z9 ) holds
z = x "\/" y
proof
let L be non empty join-commutative join-associative meet-commutative meet-absorbing join-absorbing LattStr ; ::_thesis: for x, y, z being Element of L st x [= z & y [= z & ( for z9 being Element of L st x [= z9 & y [= z9 holds
z [= z9 ) holds
z = x "\/" y
let x, y, z be Element of L; ::_thesis: ( x [= z & y [= z & ( for z9 being Element of L st x [= z9 & y [= z9 holds
z [= z9 ) implies z = x "\/" y )
assume that
A1: ( x [= z & y [= z ) and
A2: for z9 being Element of L st x [= z9 & y [= z9 holds
z [= z9 ; ::_thesis: z = x "\/" y
 ( x [= x "\/" y & y [= x "\/" y ) by LATTICES:5;
then A3: z [= x "\/" y by A2;
 x "\/" y [= z by A1, Th6;
hence  z = x "\/" y by A3, LATTICES:8; ::_thesis: verum
end;