:: FILTER_0 semantic presentation

begin

theorem :: FILTER_0:1
for L being ( ( non empty join-commutative join-associative meet-commutative meet-absorbing join-absorbing ) ( non empty join-commutative join-associative meet-commutative meet-absorbing join-absorbing ) LattStr )
for p, q, r being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) [= q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
r : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "\/" p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty join-commutative join-associative meet-commutative meet-absorbing join-absorbing ) ( non empty join-commutative join-associative meet-commutative meet-absorbing join-absorbing ) LattStr ) : ( ( ) ( non empty ) set ) ) [= r : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "\/" q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty join-commutative join-associative meet-commutative meet-absorbing join-absorbing ) ( non empty join-commutative join-associative meet-commutative meet-absorbing join-absorbing ) LattStr ) : ( ( ) ( non empty ) set ) ) ;

theorem :: FILTER_0:2
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for p, r, q being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) [= r : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\" q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ) [= r : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: FILTER_0:3
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for p, r, q being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) [= r : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) [= q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "\/" r : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ) ;

theorem :: FILTER_0:4
for L being ( ( non empty join-commutative join-associative join-absorbing ) ( non empty join-commutative join-associative join-absorbing ) LattStr )
for a, b, c, d being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) [= b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) [= d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "\/" c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty join-commutative join-associative join-absorbing ) ( non empty join-commutative join-associative join-absorbing ) LattStr ) : ( ( ) ( non empty ) set ) ) [= b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "\/" d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty join-commutative join-associative join-absorbing ) ( non empty join-commutative join-associative join-absorbing ) LattStr ) : ( ( ) ( non empty ) set ) ) ;

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

theorem :: FILTER_0:6
for L being ( ( non empty join-commutative join-associative meet-commutative meet-absorbing join-absorbing ) ( non empty join-commutative join-associative meet-commutative meet-absorbing join-absorbing ) LattStr )
for a, b, c being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) [= c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) [= c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "\/" b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty join-commutative join-associative meet-commutative meet-absorbing join-absorbing ) ( non empty join-commutative join-associative meet-commutative meet-absorbing join-absorbing ) LattStr ) : ( ( ) ( non empty ) set ) ) [= c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: FILTER_0:7
for L being ( ( non empty meet-commutative meet-associative meet-absorbing join-absorbing ) ( non empty meet-commutative meet-associative meet-absorbing join-absorbing ) LattStr )
for a, b, c being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) [= b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) [= c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) [= b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\" c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty meet-commutative meet-associative meet-absorbing join-absorbing ) ( non empty meet-commutative meet-associative meet-absorbing join-absorbing ) LattStr ) : ( ( ) ( non empty ) set ) ) ;

definition
let L be ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ;
mode Filter of L is ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Subset of ) ;
end;

theorem :: FILTER_0:8
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for S being ( ( non empty ) ( non empty ) Subset of ) holds
( S : ( ( non empty ) ( non empty ) Subset of ) is ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) iff for p, q being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( ( p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in S : ( ( non empty ) ( non empty ) Subset of ) & q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in S : ( ( non empty ) ( non empty ) Subset of ) ) iff p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\" q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ) in S : ( ( non empty ) ( non empty ) Subset of ) ) ) ;

theorem :: FILTER_0:9
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for D being ( ( non empty ) ( non empty ) Subset of ) holds
( D : ( ( non empty ) ( non empty ) Subset of ) is ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) iff ( ( for p, q being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in D : ( ( non empty ) ( non empty ) Subset of ) & q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in D : ( ( non empty ) ( non empty ) Subset of ) holds
p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\" q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ) in D : ( ( non empty ) ( non empty ) Subset of ) ) & ( for p, q being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in D : ( ( non empty ) ( non empty ) Subset of ) & p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) [= q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in D : ( ( non empty ) ( non empty ) Subset of ) ) ) ) ;

theorem :: FILTER_0:10
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for p, q being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for H being ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) st p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in H : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) holds
( p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "\/" q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ) in H : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) & q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "\/" p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ) in H : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) ;

theorem :: FILTER_0:11
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for H being ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) st L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) is ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) 1_Lattice) holds
Top L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ) in H : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ;

theorem :: FILTER_0:12
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) st L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) is ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) 1_Lattice) holds
{(Top L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty ) Element of bool the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ;

theorem :: FILTER_0:13
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st {p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty ) Element of bool the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) holds
L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) is upper-bounded ;

theorem :: FILTER_0:14
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) holds the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) is ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ;

definition
let L be ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ;
func <.L.) -> ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( ) ( ) LattStr ) ) equals :: FILTER_0:def 1
 the carrier of L : ( ( ) ( ) LattStr ) : ( ( ) ( ) set ) ;
end;

definition
let L be ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ;
let p be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
func <.p.) -> ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( ) ( ) LattStr ) ) equals :: FILTER_0:def 2
 { q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) where q is ( ( ) ( ) Element of ( ( ) ( ) set ) ) : p : ( ( Function-like V36([:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) ,L : ( ( ) ( ) LattStr ) ) ) ( Relation-like [:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) -defined L : ( ( ) ( ) LattStr ) -valued Function-like V36([:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) ,L : ( ( ) ( ) LattStr ) ) ) Element of bool [:[:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) [= q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) } ;
end;

theorem :: FILTER_0:15
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for q, p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in <.p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) .) : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) iff p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) [= q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ;

theorem :: FILTER_0:16
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for p, q being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in <.p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) .) : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) & p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "\/" q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ) in <.p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) .) : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) & q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "\/" p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ) in <.p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) .) : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) ;

theorem :: FILTER_0:17
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) st L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) is ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) 0_Lattice) holds
<.L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) .) : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) = <.(Bottom L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ) .) : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ;

definition
let L be ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ;
let F be ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ;
attr F is being_ultrafilter means :: FILTER_0:def 3
( F : ( ( Function-like V36([:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) ,L : ( ( ) ( ) LattStr ) ) ) ( Relation-like [:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) -defined L : ( ( ) ( ) LattStr ) -valued Function-like V36([:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) ,L : ( ( ) ( ) LattStr ) ) ) Element of bool [:[:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) <> the carrier of L : ( ( ) ( ) LattStr ) : ( ( ) ( ) set ) & ( for H being ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( ) ( ) LattStr ) ) st F : ( ( Function-like V36([:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) ,L : ( ( ) ( ) LattStr ) ) ) ( Relation-like [:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) -defined L : ( ( ) ( ) LattStr ) -valued Function-like V36([:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) ,L : ( ( ) ( ) LattStr ) ) ) Element of bool [:[:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) c= H : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) & H : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) <> the carrier of L : ( ( ) ( ) LattStr ) : ( ( ) ( ) set ) holds
F : ( ( Function-like V36([:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) ,L : ( ( ) ( ) LattStr ) ) ) ( Relation-like [:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) -defined L : ( ( ) ( ) LattStr ) -valued Function-like V36([:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) ,L : ( ( ) ( ) LattStr ) ) ) Element of bool [:[:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = H : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) );
end;

theorem :: FILTER_0:18
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) st L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) is lower-bounded holds
for F being ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) st F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) <> the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) holds
ex H being ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) st
( F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) c= H : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) & H : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) is being_ultrafilter ) ;

theorem :: FILTER_0:19
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st ex r being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\" r : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ) <> p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
<.p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) .) : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) <> the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ;

theorem :: FILTER_0:20
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) is ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) 0_Lattice) & p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> Bottom L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ) holds
ex H being ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) st
( p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in H : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) & H : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) is being_ultrafilter ) ;

definition
let L be ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ;
let D be ( ( non empty ) ( non empty ) Subset of ) ;
func <.D.) -> ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( ) ( ) LattStr ) ) means :: FILTER_0:def 4
( D : ( ( Function-like V36([:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) ,L : ( ( ) ( ) LattStr ) ) ) ( Relation-like [:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) -defined L : ( ( ) ( ) LattStr ) -valued Function-like V36([:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) ,L : ( ( ) ( ) LattStr ) ) ) Element of bool [:[:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) c= it : ( ( Function-like V36([:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) ,L : ( ( ) ( ) LattStr ) ) ) ( Relation-like [:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) -defined L : ( ( ) ( ) LattStr ) -valued Function-like V36([:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) ,L : ( ( ) ( ) LattStr ) ) ) Element of bool [:[:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) & ( for F being ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( ) ( ) LattStr ) ) st D : ( ( Function-like V36([:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) ,L : ( ( ) ( ) LattStr ) ) ) ( Relation-like [:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) -defined L : ( ( ) ( ) LattStr ) -valued Function-like V36([:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) ,L : ( ( ) ( ) LattStr ) ) ) Element of bool [:[:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) c= F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) holds
it : ( ( Function-like V36([:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) ,L : ( ( ) ( ) LattStr ) ) ) ( Relation-like [:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) -defined L : ( ( ) ( ) LattStr ) -valued Function-like V36([:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) ,L : ( ( ) ( ) LattStr ) ) ) Element of bool [:[:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) c= F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) );
end;

theorem :: FILTER_0:21
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for F being ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) holds <.F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) .) : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) = F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ;

theorem :: FILTER_0:22
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for D1, D2 being ( ( non empty ) ( non empty ) Subset of ) st D1 : ( ( non empty ) ( non empty ) Subset of ) c= D2 : ( ( non empty ) ( non empty ) Subset of ) holds
<.D1 : ( ( non empty ) ( non empty ) Subset of ) .) : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) c= <.D2 : ( ( non empty ) ( non empty ) Subset of ) .) : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ;

theorem :: FILTER_0:23
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for D being ( ( non empty ) ( non empty ) Subset of ) st p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in D : ( ( non empty ) ( non empty ) Subset of ) holds
<.p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) .) : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) c= <.D : ( ( non empty ) ( non empty ) Subset of ) .) : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ;

theorem :: FILTER_0:24
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for D being ( ( non empty ) ( non empty ) Subset of ) st D : ( ( non empty ) ( non empty ) Subset of ) = {p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty ) Element of bool the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) holds
<.D : ( ( non empty ) ( non empty ) Subset of ) .) : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) = <.p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) .) : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ;

theorem :: FILTER_0:25
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for D being ( ( non empty ) ( non empty ) Subset of ) st L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) is ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) 0_Lattice) & Bottom L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ) in D : ( ( non empty ) ( non empty ) Subset of ) holds
( <.D : ( ( non empty ) ( non empty ) Subset of ) .) : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) = <.L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) .) : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) & <.D : ( ( non empty ) ( non empty ) Subset of ) .) : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) = the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ) ;

theorem :: FILTER_0:26
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for F being ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) st L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) is ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) 0_Lattice) & Bottom L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ) in F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) holds
( F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) = <.L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) .) : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) & F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) = the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ) ;

definition
let L be ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ;
let F be ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ;
attr F is prime means :: FILTER_0:def 5
 for p, q being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
( p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "\/" q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of L : ( ( ) ( ) LattStr ) : ( ( ) ( ) set ) ) in F : ( ( Function-like V36([:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) ,L : ( ( ) ( ) LattStr ) ) ) ( Relation-like [:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) -defined L : ( ( ) ( ) LattStr ) -valued Function-like V36([:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) ,L : ( ( ) ( ) LattStr ) ) ) Element of bool [:[:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) iff ( p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in F : ( ( Function-like V36([:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) ,L : ( ( ) ( ) LattStr ) ) ) ( Relation-like [:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) -defined L : ( ( ) ( ) LattStr ) -valued Function-like V36([:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) ,L : ( ( ) ( ) LattStr ) ) ) Element of bool [:[:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) or q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in F : ( ( Function-like V36([:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) ,L : ( ( ) ( ) LattStr ) ) ) ( Relation-like [:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) -defined L : ( ( ) ( ) LattStr ) -valued Function-like V36([:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) ,L : ( ( ) ( ) LattStr ) ) ) Element of bool [:[:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) );
end;

theorem :: FILTER_0:27
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) st L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) is ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean ) B_Lattice) holds
for p, q being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\" ((p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ) "\/" q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ) [= q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & ( for r being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\" r : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ) [= q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
r : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) [= (p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ) "\/" q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ) ) ) ;

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

registration
cluster non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like implicative for ( ( ) ( ) LattStr ) ;
end;

definition
mode I_Lattice is ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like implicative ) Lattice) ;
end;

definition
let L be ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ;
let p, q be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
assume L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) is ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like implicative ) I_Lattice) ;
func p => q -> ( ( ) ( ) Element of ( ( ) ( ) set ) ) means :: FILTER_0:def 7
( p : ( ( Function-like V36([:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) ,L : ( ( ) ( ) LattStr ) ) ) ( Relation-like [:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) -defined L : ( ( ) ( ) LattStr ) -valued Function-like V36([:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) ,L : ( ( ) ( ) LattStr ) ) ) Element of bool [:[:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) "/\" it : ( ( ) ( ) set ) : ( ( ) ( ) Element of the carrier of L : ( ( ) ( ) LattStr ) : ( ( ) ( ) set ) ) [= q : ( ( Function-like V36([:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) ,L : ( ( ) ( ) LattStr ) ) ) ( Relation-like [:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) -defined L : ( ( ) ( ) LattStr ) -valued Function-like V36([:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) ,L : ( ( ) ( ) LattStr ) ) ) Element of bool [:[:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) & ( for r being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st p : ( ( Function-like V36([:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) ,L : ( ( ) ( ) LattStr ) ) ) ( Relation-like [:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) -defined L : ( ( ) ( ) LattStr ) -valued Function-like V36([:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) ,L : ( ( ) ( ) LattStr ) ) ) Element of bool [:[:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) "/\" r : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of L : ( ( ) ( ) LattStr ) : ( ( ) ( ) set ) ) [= q : ( ( Function-like V36([:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) ,L : ( ( ) ( ) LattStr ) ) ) ( Relation-like [:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) -defined L : ( ( ) ( ) LattStr ) -valued Function-like V36([:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) ,L : ( ( ) ( ) LattStr ) ) ) Element of bool [:[:L : ( ( ) ( ) LattStr ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) ,L : ( ( ) ( ) LattStr ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) holds
r : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) [= it : ( ( ) ( ) set ) ) );
end;

registration
cluster non empty Lattice-like implicative -> non empty Lattice-like upper-bounded implicative for ( ( ) ( ) LattStr ) ;
end;

theorem :: FILTER_0:28
for I being ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like implicative ) I_Lattice)
for i being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds i : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) => i : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = Top I : ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded implicative ) I_Lattice) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded implicative ) I_Lattice) : ( ( ) ( non empty ) set ) ) ;

registration
cluster non empty Lattice-like implicative -> non empty Lattice-like distributive implicative for ( ( ) ( ) LattStr ) ;
end;

registration
cluster non empty Lattice-like Boolean -> non empty Lattice-like Boolean implicative for ( ( ) ( ) LattStr ) ;
end;

registration
cluster non empty Lattice-like implicative -> non empty Lattice-like distributive for ( ( ) ( ) LattStr ) ;
end;

theorem :: FILTER_0:29
for I being ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative ) I_Lattice)
for i, j being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for FI being ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of I : ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative ) I_Lattice) ) st i : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in FI : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative ) I_Lattice) ) & i : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) => j : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in FI : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative ) I_Lattice) ) holds
j : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in FI : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative ) I_Lattice) ) ;

theorem :: FILTER_0:30
for I being ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative ) I_Lattice)
for j, i being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for FI being ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of I : ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative ) I_Lattice) ) st j : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in FI : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative ) I_Lattice) ) holds
i : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) => j : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in FI : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative ) I_Lattice) ) ;

definition
let L be ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ;
let D1, D2 be ( ( non empty ) ( non empty ) Subset of ) ;
func D1 "/\" D2 -> ( ( ) ( ) Subset of ) equals :: FILTER_0:def 8
 { (p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\" q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) ) where p, q is ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in D1 : ( ( ) ( ) set ) & q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in D2 : ( ( Function-like V36([:L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) ,L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) :] : ( ( ) ( ) set ) ,L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) ) ) ( Relation-like [:L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) ,L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) :] : ( ( ) ( ) set ) -defined L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) -valued Function-like V36([:L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) ,L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) :] : ( ( ) ( ) set ) ,L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) ) ) Element of bool [:[:L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) ,L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) :] : ( ( ) ( ) set ) ,L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) } ;
end;

registration
let L be ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ;
let D1, D2 be ( ( non empty ) ( non empty ) Subset of ) ;
cluster D1 : ( ( non empty ) ( non empty ) Element of bool the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) "/\" D2 : ( ( non empty ) ( non empty ) Element of bool the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ) -> non empty ;
end;

theorem :: FILTER_0:31
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for p, q being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for D1, D2 being ( ( non empty ) ( non empty ) Subset of ) st p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in D1 : ( ( non empty ) ( non empty ) Subset of ) & q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in D2 : ( ( non empty ) ( non empty ) Subset of ) holds
( p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\" q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ) in D1 : ( ( non empty ) ( non empty ) Subset of ) "/\" D2 : ( ( non empty ) ( non empty ) Subset of ) : ( ( ) ( non empty ) Subset of ) & q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\" p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ) in D1 : ( ( non empty ) ( non empty ) Subset of ) "/\" D2 : ( ( non empty ) ( non empty ) Subset of ) : ( ( ) ( non empty ) Subset of ) ) ;

theorem :: FILTER_0:32
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for x being ( ( ) ( ) set )
for D1, D2 being ( ( non empty ) ( non empty ) Subset of ) st x : ( ( ) ( ) set ) in D1 : ( ( non empty ) ( non empty ) Subset of ) "/\" D2 : ( ( non empty ) ( non empty ) Subset of ) : ( ( ) ( non empty ) Subset of ) holds
ex p, q being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( x : ( ( ) ( ) set ) = p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\" q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in D1 : ( ( non empty ) ( non empty ) Subset of ) & q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in D2 : ( ( non empty ) ( non empty ) Subset of ) ) ;

theorem :: FILTER_0:33
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for D1, D2 being ( ( non empty ) ( non empty ) Subset of ) holds D1 : ( ( non empty ) ( non empty ) Subset of ) "/\" D2 : ( ( non empty ) ( non empty ) Subset of ) : ( ( ) ( non empty ) Subset of ) = D2 : ( ( non empty ) ( non empty ) Subset of ) "/\" D1 : ( ( non empty ) ( non empty ) Subset of ) : ( ( ) ( non empty ) Subset of ) ;

registration
let L be ( ( non empty Lattice-like distributive ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular ) D_Lattice) ;
let F1, F2 be ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like distributive ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular ) D_Lattice) ) ;
cluster F1 : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Element of bool the carrier of L : ( ( non empty Lattice-like distributive ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular ) LattStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) "/\" F2 : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Element of bool the carrier of L : ( ( non empty Lattice-like distributive ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular ) LattStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Subset of ) -> final meet-closed ;
end;

theorem :: FILTER_0:34
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for D1, D2 being ( ( non empty ) ( non empty ) Subset of ) holds
( <.(D1 : ( ( non empty ) ( non empty ) Subset of ) \/ D2 : ( ( non empty ) ( non empty ) Subset of ) ) : ( ( ) ( non empty ) Element of bool the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) .) : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) = <.(<.D1 : ( ( non empty ) ( non empty ) Subset of ) .) : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) \/ D2 : ( ( non empty ) ( non empty ) Subset of ) ) : ( ( ) ( non empty ) Element of bool the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) .) : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) & <.(D1 : ( ( non empty ) ( non empty ) Subset of ) \/ D2 : ( ( non empty ) ( non empty ) Subset of ) ) : ( ( ) ( non empty ) Element of bool the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) .) : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) = <.(D1 : ( ( non empty ) ( non empty ) Subset of ) \/ <.D2 : ( ( non empty ) ( non empty ) Subset of ) .) : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) : ( ( ) ( non empty ) Element of bool the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) .) : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) ;

theorem :: FILTER_0:35
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for F, H being ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) holds <.(F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) \/ H : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) : ( ( ) ( non empty ) Element of bool the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) .) : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) = { r : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) where r is ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ex p, q being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\" q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ) [= r : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) & q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in H : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) } ;

theorem :: FILTER_0:36
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for F, H being ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) holds
( F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) c= F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) "/\" H : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) : ( ( ) ( non empty ) Subset of ) & H : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) c= F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) "/\" H : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) : ( ( ) ( non empty ) Subset of ) ) ;

theorem :: FILTER_0:37
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for F, H being ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) holds <.(F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) \/ H : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) : ( ( ) ( non empty ) Element of bool the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) .) : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) = <.(F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) "/\" H : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) : ( ( ) ( non empty ) Subset of ) .) : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ;

theorem :: FILTER_0:38
for I being ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative ) I_Lattice)
for F1, F2 being ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of I : ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative ) I_Lattice) ) holds <.(F1 : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative ) I_Lattice) ) \/ F2 : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative ) I_Lattice) ) ) : ( ( ) ( non empty ) Element of bool the carrier of b1 : ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative ) I_Lattice) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) .) : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative ) I_Lattice) ) = F1 : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative ) I_Lattice) ) "/\" F2 : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative ) I_Lattice) ) : ( ( ) ( non empty final meet-closed join-closed ) Subset of ) ;

theorem :: FILTER_0:39
for B being ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean ) B_Lattice)
for FB, HB being ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of B : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative ) B_Lattice) ) holds <.(FB : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative ) B_Lattice) ) \/ HB : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative ) B_Lattice) ) ) : ( ( ) ( non empty ) Element of bool the carrier of b1 : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative ) B_Lattice) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) .) : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative ) B_Lattice) ) = FB : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative ) B_Lattice) ) "/\" HB : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative ) B_Lattice) ) : ( ( ) ( non empty final meet-closed join-closed ) Subset of ) ;

theorem :: FILTER_0:40
for I being ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative ) I_Lattice)
for j, i being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for DI being ( ( non empty ) ( non empty ) Subset of ) st j : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in <.(DI : ( ( non empty ) ( non empty ) Subset of ) \/ {i : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty ) Element of bool the carrier of b1 : ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative ) I_Lattice) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) Element of bool the carrier of b1 : ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative ) I_Lattice) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) .) : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative ) I_Lattice) ) holds
i : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) => j : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in <.DI : ( ( non empty ) ( non empty ) Subset of ) .) : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative ) I_Lattice) ) ;

theorem :: FILTER_0:41
for I being ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative ) I_Lattice)
for i, j, k being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for FI being ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of I : ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative ) I_Lattice) ) st i : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) => j : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in FI : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative ) I_Lattice) ) & j : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) => k : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in FI : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative ) I_Lattice) ) holds
i : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) => k : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in FI : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative ) I_Lattice) ) ;

theorem :: FILTER_0:42
for B being ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean ) B_Lattice)
for a, b being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) => b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative ) B_Lattice) : ( ( ) ( non empty ) set ) ) "\/" b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative ) B_Lattice) : ( ( ) ( non empty ) set ) ) ;

theorem :: FILTER_0:43
for B being ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean ) B_Lattice)
for a, b being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) [= b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) iff a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\" (b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative ) B_Lattice) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative ) B_Lattice) : ( ( ) ( non empty ) set ) ) = Bottom B : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative ) B_Lattice) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative ) B_Lattice) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: FILTER_0:44
for B being ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean ) B_Lattice)
for FB being ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of B : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative ) B_Lattice) ) holds
( FB : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative ) B_Lattice) ) is being_ultrafilter iff ( FB : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative ) B_Lattice) ) <> the carrier of B : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative ) B_Lattice) : ( ( ) ( non empty ) set ) & ( for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in FB : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative ) B_Lattice) ) or a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ` : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative ) B_Lattice) : ( ( ) ( non empty ) set ) ) in FB : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative ) B_Lattice) ) ) ) ) ) ;

theorem :: FILTER_0:45
for B being ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean ) B_Lattice)
for FB being ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of B : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative ) B_Lattice) ) holds
( ( FB : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative ) B_Lattice) ) <> <.B : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative ) B_Lattice) .) : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative ) B_Lattice) ) & FB : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative ) B_Lattice) ) is prime ) iff FB : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative ) B_Lattice) ) is being_ultrafilter ) ;

theorem :: FILTER_0:46
for B being ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean ) B_Lattice)
for FB being ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of B : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative ) B_Lattice) ) st FB : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative ) B_Lattice) ) is being_ultrafilter holds
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in FB : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative ) B_Lattice) ) iff not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ` : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative ) B_Lattice) : ( ( ) ( non empty ) set ) ) in FB : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative ) B_Lattice) ) ) ;

theorem :: FILTER_0:47
for B being ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean ) B_Lattice)
for a, b being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
ex FB being ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of B : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative ) B_Lattice) ) st
( FB : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative ) B_Lattice) ) is being_ultrafilter & ( ( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in FB : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative ) B_Lattice) ) & not b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in FB : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative ) B_Lattice) ) ) or ( not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in FB : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative ) B_Lattice) ) & b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in FB : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative ) B_Lattice) ) ) ) ) ;

definition
let L be ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ;
let F be ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ;
func latt F -> ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) means :: FILTER_0:def 9
 ex o1, o2 being ( ( Function-like V36([:F : ( ( ) ( ) set ) ,F : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,F : ( ( ) ( ) set ) ) ) ( Relation-like [:F : ( ( ) ( ) set ) ,F : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) -defined F : ( ( ) ( ) set ) -valued Function-like V36([:F : ( ( ) ( ) set ) ,F : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) ,F : ( ( ) ( ) set ) ) ) BinOp of F : ( ( ) ( ) set ) ) st
( o1 : ( ( Function-like V36([:F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ,F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) :] : ( ( ) ( non empty ) set ) ,F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) ) ( Relation-like [:F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ,F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) :] : ( ( ) ( non empty ) set ) -defined F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) -valued Function-like V36([:F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ,F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) :] : ( ( ) ( non empty ) set ) ,F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) ) BinOp of F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) = the L_join of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( Function-like V36([: the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like [: the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) -valued Function-like V36([: the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) ) ) Element of bool [:[: the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) || F : ( ( ) ( ) set ) : ( ( ) ( ) set ) & o2 : ( ( Function-like V36([:F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ,F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) :] : ( ( ) ( non empty ) set ) ,F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) ) ( Relation-like [:F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ,F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) :] : ( ( ) ( non empty ) set ) -defined F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) -valued Function-like V36([:F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ,F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) :] : ( ( ) ( non empty ) set ) ,F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) ) BinOp of F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) = the L_meet of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( Function-like V36([: the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like [: the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) -valued Function-like V36([: the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) ) ) Element of bool [:[: the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) || F : ( ( ) ( ) set ) : ( ( ) ( ) set ) & it : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Element of bool the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = LattStr(# F : ( ( ) ( ) set ) ,o1 : ( ( Function-like V36([:F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ,F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) :] : ( ( ) ( non empty ) set ) ,F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) ) ( Relation-like [:F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ,F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) :] : ( ( ) ( non empty ) set ) -defined F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) -valued Function-like V36([:F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ,F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) :] : ( ( ) ( non empty ) set ) ,F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) ) BinOp of F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) ,o2 : ( ( Function-like V36([:F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ,F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) :] : ( ( ) ( non empty ) set ) ,F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) ) ( Relation-like [:F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ,F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) :] : ( ( ) ( non empty ) set ) -defined F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) -valued Function-like V36([:F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ,F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) :] : ( ( ) ( non empty ) set ) ,F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) ) BinOp of F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) #) : ( ( strict ) ( strict ) LattStr ) );
end;

registration
let L be ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ;
let F be ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ;
cluster latt F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Element of bool the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) -> non empty strict Lattice-like ;
end;

theorem :: FILTER_0:48
for L being ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) holds latt <.L : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) .) : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) : ( ( non empty Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) = L : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ;

theorem :: FILTER_0:49
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for F being ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) holds
( the carrier of (latt F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) : ( ( non empty Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) = F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) & the L_join of (latt F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) : ( ( non empty Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( Function-like V36([: the carrier of (latt b2 : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) : ( ( non empty Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) , the carrier of (latt b2 : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) : ( ( non empty Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of (latt b2 : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) : ( ( non empty Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ) ) ( Relation-like [: the carrier of (latt b2 : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) : ( ( non empty Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) , the carrier of (latt b2 : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) : ( ( non empty Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined the carrier of (latt b2 : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) : ( ( non empty Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) -valued Function-like V36([: the carrier of (latt b2 : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) : ( ( non empty Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) , the carrier of (latt b2 : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) : ( ( non empty Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of (latt b2 : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) : ( ( non empty Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ) ) Element of bool [:[: the carrier of (latt b2 : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) : ( ( non empty Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) , the carrier of (latt b2 : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) : ( ( non empty Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of (latt b2 : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) : ( ( non empty Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = the L_join of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( Function-like V36([: the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ) ) ( Relation-like [: the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) -valued Function-like V36([: the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ) ) Element of bool [:[: the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) || F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) : ( ( ) ( ) set ) & the L_meet of (latt F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) : ( ( non empty Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( Function-like V36([: the carrier of (latt b2 : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) : ( ( non empty Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) , the carrier of (latt b2 : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) : ( ( non empty Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of (latt b2 : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) : ( ( non empty Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ) ) ( Relation-like [: the carrier of (latt b2 : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) : ( ( non empty Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) , the carrier of (latt b2 : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) : ( ( non empty Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined the carrier of (latt b2 : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) : ( ( non empty Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) -valued Function-like V36([: the carrier of (latt b2 : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) : ( ( non empty Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) , the carrier of (latt b2 : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) : ( ( non empty Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of (latt b2 : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) : ( ( non empty Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ) ) Element of bool [:[: the carrier of (latt b2 : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) : ( ( non empty Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) , the carrier of (latt b2 : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) : ( ( non empty Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of (latt b2 : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) : ( ( non empty Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = the L_meet of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( Function-like V36([: the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ) ) ( Relation-like [: the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) -valued Function-like V36([: the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ) ) Element of bool [:[: the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) || F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) : ( ( ) ( ) set ) ) ;

theorem :: FILTER_0:50
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for p, q being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for F being ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) )
for p9, q9 being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = p9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = q9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "\/" q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ) = p9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "\/" q9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (latt b4 : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) : ( ( non empty Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\" q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ) = p9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\" q9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (latt b4 : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) : ( ( non empty Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: FILTER_0:51
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for p, q being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for F being ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) )
for p9, q9 being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = p9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = q9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) [= q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) iff p9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) [= q9 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ;

theorem :: FILTER_0:52
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for F being ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) st L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) is upper-bounded holds
latt F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) : ( ( non empty Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) is upper-bounded ;

theorem :: FILTER_0:53
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for F being ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) st L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) is modular holds
latt F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) : ( ( non empty Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) is modular ;

theorem :: FILTER_0:54
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for F being ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) st L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) is distributive holds
latt F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) : ( ( non empty Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) is distributive ;

theorem :: FILTER_0:55
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for F being ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) st L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) is ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative ) I_Lattice) holds
latt F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) : ( ( non empty Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) is implicative ;

registration
let L be ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ;
let p be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
cluster latt <.p : ( ( ) ( ) Element of the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) ) .) : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) ) : ( ( non empty Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) -> non empty Lattice-like lower-bounded ;
end;

theorem :: FILTER_0:56
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds Bottom (latt <.p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) .) : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) : ( ( non empty Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) : ( ( ) ( ) Element of the carrier of (latt <.b2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) .) : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) : ( ( non empty Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) = p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: FILTER_0:57
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) is upper-bounded holds
Top (latt <.p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) .) : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) : ( ( non empty Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) : ( ( ) ( ) Element of the carrier of (latt <.b2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) .) : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) : ( ( non empty Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) = Top L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ) ;

theorem :: FILTER_0:58
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) is ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) 1_Lattice) holds
latt <.p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) .) : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) : ( ( non empty Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) is bounded ;

theorem :: FILTER_0:59
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) is ( ( non empty Lattice-like bounded complemented ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complemented ) C_Lattice) & L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) is ( ( non empty Lattice-like modular ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like modular ) M_Lattice) holds
latt <.p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) .) : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) : ( ( non empty Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) is ( ( non empty Lattice-like bounded complemented ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded bounded complemented ) C_Lattice) ;

theorem :: FILTER_0:60
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) is ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative ) B_Lattice) holds
latt <.p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) .) : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) : ( ( non empty Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) is ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative ) B_Lattice) ;

definition
let L be ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ;
let p, q be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
func p <=> q -> ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) equals :: FILTER_0:def 10
(p : ( ( ) ( ) set ) => q : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Element of bool the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\" (q : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Element of bool the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) => p : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: FILTER_0:61
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for p, q being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <=> q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <=> p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: FILTER_0:62
for I being ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative ) I_Lattice)
for i, j, k being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for FI being ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of I : ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative ) I_Lattice) ) st i : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <=> j : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in FI : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative ) I_Lattice) ) & j : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <=> k : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in FI : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative ) I_Lattice) ) holds
i : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <=> k : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in FI : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative ) I_Lattice) ) ;

definition
let L be ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ;
let F be ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ;
func equivalence_wrt F -> ( ( Relation-like ) ( Relation-like ) Relation) means :: FILTER_0:def 11
( field it : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Element of bool the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) c= the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) & ( for p, q being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( [p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( V33() ) Element of [: the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ) in it : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Element of bool the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) iff p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <=> q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in F : ( ( ) ( ) set ) ) ) );
end;

theorem :: FILTER_0:63
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for F being ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) holds equivalence_wrt F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) : ( ( Relation-like ) ( Relation-like ) Relation) is ( ( ) ( Relation-like the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) -valued ) Relation of ) ;

theorem :: FILTER_0:64
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for F being ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) st L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) is ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative ) I_Lattice) holds
equivalence_wrt F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) : ( ( Relation-like ) ( Relation-like ) Relation) is_reflexive_in the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ;

theorem :: FILTER_0:65
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for F being ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) holds equivalence_wrt F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) : ( ( Relation-like ) ( Relation-like ) Relation) is_symmetric_in the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ;

theorem :: FILTER_0:66
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for F being ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) st L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) is ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative ) I_Lattice) holds
equivalence_wrt F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) : ( ( Relation-like ) ( Relation-like ) Relation) is_transitive_in the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ;

theorem :: FILTER_0:67
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for F being ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) st L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) is ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative ) I_Lattice) holds
equivalence_wrt F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) : ( ( Relation-like ) ( Relation-like ) Relation) is ( ( symmetric transitive V32( the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) -valued symmetric transitive V32( the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ) ) Equivalence_Relation of the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ) ;

theorem :: FILTER_0:68
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for F being ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) st L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) is ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative ) I_Lattice) holds
field (equivalence_wrt F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) = the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ;

definition
let I be ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative ) I_Lattice) ;
let FI be ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of I : ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative ) I_Lattice) ) ;
:: original: equivalence_wrt
redefine func equivalence_wrt FI -> ( ( symmetric transitive V32( the carrier of I : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of I : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) -defined the carrier of I : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) -valued symmetric transitive V32( the carrier of I : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) ) ) Equivalence_Relation of the carrier of I : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) ) ;
end;

definition
let B be ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean ) B_Lattice) ;
let FB be ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of B : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative ) B_Lattice) ) ;
:: original: equivalence_wrt
redefine func equivalence_wrt FB -> ( ( symmetric transitive V32( the carrier of B : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of B : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) -defined the carrier of B : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) -valued symmetric transitive V32( the carrier of B : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) ) ) Equivalence_Relation of the carrier of B : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) ) ;
end;

definition
let L be ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ;
let F be ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ;
let p, q be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
pred p,q are_equivalence_wrt F means :: FILTER_0:def 12
p : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Element of bool the carrier of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) <=> q : ( ( ) ( ) set ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in F : ( ( ) ( ) set ) ;
end;

theorem :: FILTER_0:69
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for p, q being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for F being ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) holds
( p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) are_equivalence_wrt F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) iff [p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ] : ( ( ) ( V33() ) Element of [: the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ) in equivalence_wrt F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) : ( ( Relation-like ) ( Relation-like ) Relation) ) ;

theorem :: FILTER_0:70
for B being ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean ) B_Lattice)
for FB being ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of B : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative ) B_Lattice) )
for I being ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative ) I_Lattice)
for i being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for FI being ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of I : ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative ) I_Lattice) )
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( i : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,i : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) are_equivalence_wrt FI : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b3 : ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative ) I_Lattice) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) are_equivalence_wrt FB : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative ) B_Lattice) ) ) ;

theorem :: FILTER_0:71
for L being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for p, q being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for F being ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) st p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) are_equivalence_wrt F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) holds
q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) are_equivalence_wrt F : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ;

theorem :: FILTER_0:72
for B being ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean ) B_Lattice)
for FB being ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of B : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative ) B_Lattice) )
for I being ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative ) I_Lattice)
for i, j, k being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for FI being ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of I : ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative ) I_Lattice) )
for a, b, c being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( ( i : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,j : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) are_equivalence_wrt FI : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b3 : ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative ) I_Lattice) ) & j : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,k : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) are_equivalence_wrt FI : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b3 : ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative ) I_Lattice) ) implies i : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,k : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) are_equivalence_wrt FI : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b3 : ( ( non empty Lattice-like implicative ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded implicative ) I_Lattice) ) ) & ( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) are_equivalence_wrt FB : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative ) B_Lattice) ) & b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) are_equivalence_wrt FB : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative ) B_Lattice) ) implies a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ,c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) are_equivalence_wrt FB : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) Filter of b1 : ( ( non empty Lattice-like Boolean ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded complemented Boolean implicative ) B_Lattice) ) ) ) ;

begin

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

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