:: LATTICE4 semantic presentation

begin

theorem :: LATTICE4:1
for X being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) <> {} : ( ( ) ( empty ) set ) & ( for Z being ( ( ) ( ) set ) st Z : ( ( ) ( ) set ) <> {} : ( ( ) ( empty ) set ) & Z : ( ( ) ( ) set ) c= X : ( ( ) ( ) set ) & Z : ( ( ) ( ) set ) is c=-linear holds
ex Y being ( ( ) ( ) set ) st
( Y : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) & ( for X1 being ( ( ) ( ) set ) st X1 : ( ( ) ( ) set ) in Z : ( ( ) ( ) set ) holds
X1 : ( ( ) ( ) set ) c= Y : ( ( ) ( ) set ) ) ) ) holds
ex Y being ( ( ) ( ) set ) st
( Y : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) & ( for Z being ( ( ) ( ) set ) st Z : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) & Z : ( ( ) ( ) set ) <> Y : ( ( ) ( ) set ) holds
not Y : ( ( ) ( ) set ) c= Z : ( ( ) ( ) set ) ) ) ;

begin

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) ;
cluster <.L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) .) : ( ( 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 final meet-closed prime ;
end;

theorem :: LATTICE4: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 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 ) 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 ) 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 ) ) & 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 ) 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 ) 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 ) ) ) ;

theorem :: LATTICE4: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 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 p, q being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in <.(<.q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) .) : ( ( non empty final meet-closed ) ( non empty final meet-closed join-closed ) 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 ) ) \/ 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 ) 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 ) 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
ex r being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( r : ( ( ) ( ) 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 ) ) "/\" 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 ) ) ) ;

definition
let L1, L2 be ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ;
mode Homomorphism of L1,L2 -> ( ( Function-like quasi_total ) ( Relation-like the carrier of L1 : ( ( 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 L2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like non empty V19( the carrier of L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of the carrier of L1 : ( ( 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 L2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) means :: LATTICE4:def 1
 for a1, b1 being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( it : ( ( Function-like quasi_total ) ( Relation-like [:L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) ,L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) :] : ( ( ) ( ) set ) -defined L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) -valued Function-like quasi_total ) Element of bool [:[:L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) ,L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) :] : ( ( ) ( ) set ) ,L1 : ( ( 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 ) ) . (a1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "\/" b1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of L1 : ( ( 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 the carrier of L2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) = (it : ( ( Function-like quasi_total ) ( Relation-like [:L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) ,L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) :] : ( ( ) ( ) set ) -defined L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) -valued Function-like quasi_total ) Element of bool [:[:L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) ,L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) :] : ( ( ) ( ) set ) ,L1 : ( ( 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 ) ) . a1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of L2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) "\/" (it : ( ( Function-like quasi_total ) ( Relation-like [:L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) ,L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) :] : ( ( ) ( ) set ) -defined L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) -valued Function-like quasi_total ) Element of bool [:[:L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) ,L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) :] : ( ( ) ( ) set ) ,L1 : ( ( 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 ) ) . b1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of L2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of L2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) & it : ( ( Function-like quasi_total ) ( Relation-like [:L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) ,L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) :] : ( ( ) ( ) set ) -defined L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) -valued Function-like quasi_total ) Element of bool [:[:L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) ,L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) :] : ( ( ) ( ) set ) ,L1 : ( ( 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 ) ) . (a1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\" b1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of L1 : ( ( 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 the carrier of L2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) = (it : ( ( Function-like quasi_total ) ( Relation-like [:L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) ,L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) :] : ( ( ) ( ) set ) -defined L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) -valued Function-like quasi_total ) Element of bool [:[:L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) ,L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) :] : ( ( ) ( ) set ) ,L1 : ( ( 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 ) ) . a1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of L2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) "/\" (it : ( ( Function-like quasi_total ) ( Relation-like [:L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) ,L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) :] : ( ( ) ( ) set ) -defined L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) -valued Function-like quasi_total ) Element of bool [:[:L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) ,L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) :] : ( ( ) ( ) set ) ,L1 : ( ( 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 ) ) . b1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of L2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of L2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) );
end;

theorem :: LATTICE4:4
for L1, L2 being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for a1, b1 being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for f being ( ( ) ( 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 b2 : ( ( 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 non empty V19( 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 ) ) quasi_total ) Homomorphism of L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ,L2 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) st a1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) [= b1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
f : ( ( ) ( 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 b2 : ( ( 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 non empty V19( 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 ) ) quasi_total ) Homomorphism of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ,b2 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) . a1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( 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 : ( ( ) ( 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 b2 : ( ( 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 non empty V19( 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 ) ) quasi_total ) Homomorphism of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ,b2 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) . b1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( 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 :: LATTICE4:5
for L1, L2 being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for a1, b1 being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for f being ( ( ) ( 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 b2 : ( ( 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 non empty V19( 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 ) ) quasi_total ) Homomorphism of L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ,L2 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) st f : ( ( ) ( 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 b2 : ( ( 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 non empty V19( 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 ) ) quasi_total ) Homomorphism of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ,b2 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) is one-to-one holds
( a1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) [= b1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) iff f : ( ( ) ( 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 b2 : ( ( 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 non empty V19( 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 ) ) quasi_total ) Homomorphism of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ,b2 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) . a1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( 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 : ( ( ) ( 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 b2 : ( ( 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 non empty V19( 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 ) ) quasi_total ) Homomorphism of b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ,b2 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) . b1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( 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 :: LATTICE4:6
for L1, L2 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 ( ( Function-like quasi_total ) ( 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 b2 : ( ( 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 non empty V19( 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 ) ) quasi_total ) Function of the carrier of L1 : ( ( 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 L2 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( 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 b2 : ( ( 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 non empty V19( 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 ) ) quasi_total ) Function 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 b2 : ( ( 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 onto holds
for a2 being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ex a1 being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = f : ( ( Function-like quasi_total ) ( 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 b2 : ( ( 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 non empty V19( 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 ) ) quasi_total ) Function 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 b2 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ) . a1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( 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 L1, L2 be ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ;
redefine pred L1,L2 are_isomorphic means :: LATTICE4:def 2
 ex f being ( ( ) ( Relation-like the carrier of L1 : ( ( 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 L2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like non empty V19( the carrier of L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Homomorphism of L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) ,L2 : ( ( ) ( ) set ) ) st f : ( ( ) ( Relation-like the carrier of L1 : ( ( 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 L2 : ( ( 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 non empty V19( the carrier of L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) Homomorphism of L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ,L2 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) is bijective ;
end;

definition
let L1, L2 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 ( ( ) ( Relation-like the carrier of L1 : ( ( 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 L2 : ( ( 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 non empty V19( the carrier of L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) Homomorphism of L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ,L2 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ;
pred f preserves_implication means :: LATTICE4:def 3
 for a1, b1 being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds f : ( ( Function-like quasi_total ) ( Relation-like [:L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) ,L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) :] : ( ( ) ( ) set ) -defined L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) -valued Function-like quasi_total ) Element of bool [:[:L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) ,L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) :] : ( ( ) ( ) set ) ,L1 : ( ( 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 ) ) . (a1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) => b1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of L1 : ( ( 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 the carrier of L2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) = (f : ( ( Function-like quasi_total ) ( Relation-like [:L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) ,L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) :] : ( ( ) ( ) set ) -defined L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) -valued Function-like quasi_total ) Element of bool [:[:L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) ,L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) :] : ( ( ) ( ) set ) ,L1 : ( ( 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 ) ) . a1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of L2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) => (f : ( ( Function-like quasi_total ) ( Relation-like [:L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) ,L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) :] : ( ( ) ( ) set ) -defined L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) -valued Function-like quasi_total ) Element of bool [:[:L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) ,L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) :] : ( ( ) ( ) set ) ,L1 : ( ( 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 ) ) . b1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of L2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of L2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ;
pred f preserves_top means :: LATTICE4:def 4
f : ( ( Function-like quasi_total ) ( Relation-like [:L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) ,L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) :] : ( ( ) ( ) set ) -defined L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) -valued Function-like quasi_total ) Element of bool [:[:L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) ,L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) :] : ( ( ) ( ) set ) ,L1 : ( ( 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 ) ) . (Top L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) ) : ( ( ) ( ) Element of the carrier of L1 : ( ( 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 the carrier of L2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) = Top L2 : ( ( ) ( ) set ) : ( ( ) ( ) Element of the carrier of L2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ;
pred f preserves_bottom means :: LATTICE4:def 5
f : ( ( Function-like quasi_total ) ( Relation-like [:L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) ,L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) :] : ( ( ) ( ) set ) -defined L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) -valued Function-like quasi_total ) Element of bool [:[:L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) ,L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) :] : ( ( ) ( ) set ) ,L1 : ( ( 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 ) ) . (Bottom L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) ) : ( ( ) ( ) Element of the carrier of L1 : ( ( 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 the carrier of L2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) = Bottom L2 : ( ( ) ( ) set ) : ( ( ) ( ) Element of the carrier of L2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ;
pred f preserves_complement means :: LATTICE4:def 6
 for a1 being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds f : ( ( Function-like quasi_total ) ( Relation-like [:L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) ,L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) :] : ( ( ) ( ) set ) -defined L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) -valued Function-like quasi_total ) Element of bool [:[:L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) ,L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) :] : ( ( ) ( ) set ) ,L1 : ( ( 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 ) ) . (a1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of the carrier of L1 : ( ( 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 the carrier of L2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) = (f : ( ( Function-like quasi_total ) ( Relation-like [:L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) ,L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) :] : ( ( ) ( ) set ) -defined L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) -valued Function-like quasi_total ) Element of bool [:[:L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) ,L1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) :] : ( ( ) ( ) set ) ,L1 : ( ( 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 ) ) . a1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of L2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ` : ( ( ) ( ) Element of the carrier of L2 : ( ( ) ( ) set ) : ( ( ) ( ) 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) ;
mode ClosedSubset of L is ( ( meet-closed join-closed ) ( meet-closed join-closed ) Subset of ) ;
end;

theorem :: LATTICE4:7
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 ( ( meet-closed join-closed ) ( meet-closed join-closed ) ClosedSubset of L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) ;

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) ;
cluster non empty meet-closed join-closed for ( ( ) ( ) 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 ) ) ;
end;

theorem :: LATTICE4: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 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) ) is ( ( meet-closed join-closed ) ( meet-closed join-closed ) ClosedSubset 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) ;
let B be ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) ;
func FinJoin B -> ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) equals :: LATTICE4:def 7
 FinJoin (B : ( ( ) ( ) set ) ,(id L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) ) : ( ( Function-like quasi_total ) ( 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 ) -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 non empty V19( 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 ) ) quasi_total ) 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 ) : ( ( ) ( 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 ) ) ;
func FinMeet B -> ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) equals :: LATTICE4:def 8
 FinMeet (B : ( ( ) ( ) set ) ,(id L : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) ) : ( ( Function-like quasi_total ) ( 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 ) -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 non empty V19( 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 ) ) quasi_total ) 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 ) : ( ( ) ( 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 :: LATTICE4: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 p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds FinJoin {.p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) .} : ( ( ) ( non empty ) Element of Fin 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 ) : ( ( preBoolean ) ( preBoolean ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: LATTICE4: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 being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds FinMeet {.p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) .} : ( ( ) ( non empty ) Element of Fin 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 ) : ( ( preBoolean ) ( preBoolean ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

begin

theorem :: LATTICE4:11
for L2 being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for DL being ( ( non empty Lattice-like distributive ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular ) Lattice)
for f being ( ( ) ( Relation-like the carrier of b2 : ( ( non empty Lattice-like distributive ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular ) 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 Function-like non empty V19( the carrier of b2 : ( ( non empty Lattice-like distributive ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) Homomorphism of DL : ( ( non empty Lattice-like distributive ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular ) Lattice) ,L2 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) st f : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty Lattice-like distributive ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular ) 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 Function-like non empty V19( the carrier of b2 : ( ( non empty Lattice-like distributive ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) Homomorphism of b2 : ( ( non empty Lattice-like distributive ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular ) Lattice) ,b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) is onto holds
L2 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) is distributive ;

begin

theorem :: LATTICE4:12
for L2 being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for 0L being ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice)
for f being ( ( ) ( Relation-like the carrier of b2 : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) 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 Function-like non empty V19( the carrier of b2 : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) Homomorphism of 0L : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) ,L2 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) st f : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) 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 Function-like non empty V19( the carrier of b2 : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) Homomorphism of b2 : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) ,b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) is onto holds
( L2 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) is lower-bounded & f : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) 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 Function-like non empty V19( the carrier of b2 : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) Homomorphism of b2 : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) ,b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) preserves_bottom ) ;

theorem :: LATTICE4:13
for 0L being ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice)
for B being ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) )
for b being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) : ( ( ) ( non empty ) set ) -valued Function-like non empty V19( the carrier of b1 : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) UnOp of the carrier of 0L : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) holds FinJoin ((B : ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) \/ {.b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) .} : ( ( ) ( non empty ) Element of Fin the carrier of b1 : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) : ( ( ) ( non empty ) set ) : ( ( preBoolean ) ( preBoolean ) set ) ) ) : ( ( ) ( non empty ) Element of Fin the carrier of b1 : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) : ( ( ) ( non empty ) set ) : ( ( preBoolean ) ( preBoolean ) set ) ) ,f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) : ( ( ) ( non empty ) set ) -valued Function-like non empty V19( the carrier of b1 : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) UnOp of the carrier of b1 : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) = (FinJoin (B : ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) ,f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) : ( ( ) ( non empty ) set ) -valued Function-like non empty V19( the carrier of b1 : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) UnOp of the carrier of b1 : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) "\/" (f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) : ( ( ) ( non empty ) set ) -valued Function-like non empty V19( the carrier of b1 : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) UnOp of the carrier of b1 : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) . b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) ;

theorem :: LATTICE4:14
for 0L being ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice)
for B being ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) )
for b being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds FinJoin (B : ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) \/ {.b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) .} : ( ( ) ( non empty ) Element of Fin the carrier of b1 : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) : ( ( ) ( non empty ) set ) : ( ( preBoolean ) ( preBoolean ) set ) ) ) : ( ( ) ( non empty ) Element of Fin the carrier of b1 : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) : ( ( ) ( non empty ) set ) : ( ( preBoolean ) ( preBoolean ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = (FinJoin B : ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "\/" b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) ;

theorem :: LATTICE4:15
for 0L being ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice)
for B1, B2 being ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) holds (FinJoin B1 : ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "\/" (FinJoin B2 : ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) = FinJoin (B1 : ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) \/ B2 : ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) ) : ( ( ) ( ) Element of Fin the carrier of b1 : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) : ( ( ) ( non empty ) set ) : ( ( preBoolean ) ( preBoolean ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: LATTICE4:16
for 0L being ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) holds FinJoin ({}. the carrier of 0L : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) : ( ( empty ) ( empty ) Element of Fin the carrier of b1 : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) : ( ( ) ( non empty ) set ) : ( ( preBoolean ) ( preBoolean ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = Bottom 0L : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) ;

theorem :: LATTICE4:17
for 0L being ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice)
for A being ( ( meet-closed join-closed ) ( meet-closed join-closed ) ClosedSubset of 0L : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) ) st Bottom 0L : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) in A : ( ( meet-closed join-closed ) ( meet-closed join-closed ) ClosedSubset of b1 : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) ) holds
for B being ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) st B : ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) c= A : ( ( meet-closed join-closed ) ( meet-closed join-closed ) ClosedSubset of b1 : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) ) holds
FinJoin B : ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in A : ( ( meet-closed join-closed ) ( meet-closed join-closed ) ClosedSubset of b1 : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) ) ;

begin

theorem :: LATTICE4:18
for L2 being ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice)
for 1L being ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice)
for f being ( ( ) ( Relation-like the carrier of b2 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) 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 Function-like non empty V19( the carrier of b2 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) Homomorphism of 1L : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) ,L2 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) st f : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) 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 Function-like non empty V19( the carrier of b2 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) Homomorphism of b2 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) ,b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) is onto holds
( L2 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) is upper-bounded & f : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) 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 Function-like non empty V19( the carrier of b2 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) Homomorphism of b2 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) ,b1 : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) Lattice) ) preserves_top ) ;

theorem :: LATTICE4:19
for 1L being ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) holds FinMeet ({}. the carrier of 1L : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) : ( ( empty ) ( empty ) Element of Fin the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) : ( ( preBoolean ) ( preBoolean ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = Top 1L : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) ;

theorem :: LATTICE4:20
for 1L being ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice)
for B being ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) )
for b being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for f being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) -valued Function-like non empty V19( the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) UnOp of the carrier of 1L : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) holds FinMeet ((B : ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) \/ {.b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) .} : ( ( ) ( non empty ) Element of Fin the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) : ( ( preBoolean ) ( preBoolean ) set ) ) ) : ( ( ) ( non empty ) Element of Fin the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) : ( ( preBoolean ) ( preBoolean ) set ) ) ,f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) -valued Function-like non empty V19( the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) UnOp of the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) = (FinMeet (B : ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) ,f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) -valued Function-like non empty V19( the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) UnOp of the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) )) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) "/\" (f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) -valued Function-like non empty V19( the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) UnOp of the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) . b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) ;

theorem :: LATTICE4:21
for 1L being ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice)
for B being ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) )
for b being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds FinMeet (B : ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) \/ {.b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) .} : ( ( ) ( non empty ) Element of Fin the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) : ( ( preBoolean ) ( preBoolean ) set ) ) ) : ( ( ) ( non empty ) Element of Fin the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) : ( ( preBoolean ) ( preBoolean ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = (FinMeet B : ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\" b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) ;

theorem :: LATTICE4:22
for 1L being ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice)
for B being ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) )
for f, g being ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) -valued Function-like non empty V19( the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) UnOp of the carrier of 1L : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) holds FinMeet ((f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) -valued Function-like non empty V19( the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) UnOp of the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) .: B : ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) ) : ( ( ) ( ) Element of Fin the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) : ( ( preBoolean ) ( preBoolean ) set ) ) ,g : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) -valued Function-like non empty V19( the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) UnOp of the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) = FinMeet (B : ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) ,(g : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) -valued Function-like non empty V19( the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) UnOp of the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) * f : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) -valued Function-like non empty V19( the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) UnOp of the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( Relation-like the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) -valued Function-like non empty V19( the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) ;

theorem :: LATTICE4:23
for 1L being ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice)
for B1, B2 being ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) holds (FinMeet B1 : ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\" (FinMeet B2 : ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) = FinMeet (B1 : ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) \/ B2 : ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) ) : ( ( ) ( ) Element of Fin the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) : ( ( preBoolean ) ( preBoolean ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: LATTICE4:24
for 1L being ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice)
for F being ( ( meet-closed join-closed ) ( meet-closed join-closed ) ClosedSubset of 1L : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) ) st Top 1L : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) in F : ( ( meet-closed join-closed ) ( meet-closed join-closed ) ClosedSubset of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) ) holds
for B being ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) st B : ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) c= F : ( ( meet-closed join-closed ) ( meet-closed join-closed ) ClosedSubset of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) ) holds
FinMeet B : ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in F : ( ( meet-closed join-closed ) ( meet-closed join-closed ) ClosedSubset of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) ) ;

begin

theorem :: LATTICE4:25
for DL being ( ( non empty Lattice-like distributive upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded ) Lattice)
for B being ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) )
for p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds (FinMeet B : ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "\/" p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like distributive upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) = FinMeet (( the L_join of DL : ( ( non empty Lattice-like distributive upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded ) Lattice) : ( ( Function-like quasi_total ) ( Relation-like [: the carrier of b1 : ( ( non empty Lattice-like distributive upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty Lattice-like distributive upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty Lattice-like distributive upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) -valued Function-like non empty V19([: the carrier of b1 : ( ( non empty Lattice-like distributive upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty Lattice-like distributive upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) ) quasi_total commutative associative idempotent ) Element of bool [:[: the carrier of b1 : ( ( non empty Lattice-like distributive upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty Lattice-like distributive upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty Lattice-like distributive upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) [:] ((id DL : ( ( non empty Lattice-like distributive upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded ) Lattice) ) : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty Lattice-like distributive upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty Lattice-like distributive upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) -valued Function-like non empty V19( the carrier of b1 : ( ( non empty Lattice-like distributive upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier of b1 : ( ( non empty Lattice-like distributive upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty Lattice-like distributive upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) )) : ( ( Function-like quasi_total ) ( Relation-like the carrier of b1 : ( ( non empty Lattice-like distributive upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty Lattice-like distributive upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) -valued Function-like non empty V19( the carrier of b1 : ( ( non empty Lattice-like distributive upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of bool [: the carrier of b1 : ( ( non empty Lattice-like distributive upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty Lattice-like distributive upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) .: B : ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) ) : ( ( ) ( ) Element of Fin the carrier of b1 : ( ( non empty Lattice-like distributive upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) : ( ( preBoolean ) ( preBoolean ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

begin

theorem :: LATTICE4:26
for CL being ( ( 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)
for IL 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 ) Lattice)
for f being ( ( ) ( Relation-like the carrier of b2 : ( ( 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 ) Lattice) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( 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) : ( ( ) ( non empty ) set ) -valued Function-like non empty V19( the carrier of b2 : ( ( 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 ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) Homomorphism of IL : ( ( 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 ) Lattice) ,CL : ( ( 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) )
for i, j being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds (f : ( ( ) ( Relation-like the carrier of b2 : ( ( 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 ) Lattice) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( 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) : ( ( ) ( non empty ) set ) -valued Function-like non empty V19( the carrier of b2 : ( ( 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 ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) Homomorphism of b2 : ( ( 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 ) Lattice) ,b1 : ( ( 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) ) . i : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( 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) : ( ( ) ( non empty ) set ) ) "/\" (f : ( ( ) ( Relation-like the carrier of b2 : ( ( 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 ) Lattice) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( 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) : ( ( ) ( non empty ) set ) -valued Function-like non empty V19( the carrier of b2 : ( ( 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 ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) Homomorphism of b2 : ( ( 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 ) Lattice) ,b1 : ( ( 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) ) . (i : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) => j : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( 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 ) Lattice) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( 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) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( 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) : ( ( ) ( non empty ) set ) ) [= f : ( ( ) ( Relation-like the carrier of b2 : ( ( 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 ) Lattice) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( 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) : ( ( ) ( non empty ) set ) -valued Function-like non empty V19( the carrier of b2 : ( ( 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 ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) Homomorphism of b2 : ( ( 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 ) Lattice) ,b1 : ( ( 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) ) . j : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( 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) : ( ( ) ( non empty ) set ) ) ;

theorem :: LATTICE4:27
for CL being ( ( 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)
for IL 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 ) Lattice)
for f being ( ( ) ( Relation-like the carrier of b2 : ( ( 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 ) Lattice) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( 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) : ( ( ) ( non empty ) set ) -valued Function-like non empty V19( the carrier of b2 : ( ( 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 ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) Homomorphism of IL : ( ( 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 ) Lattice) ,CL : ( ( 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) )
for i, k, j being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st f : ( ( ) ( Relation-like the carrier of b2 : ( ( 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 ) Lattice) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( 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) : ( ( ) ( non empty ) set ) -valued Function-like non empty V19( the carrier of b2 : ( ( 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 ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) Homomorphism of b2 : ( ( 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 ) Lattice) ,b1 : ( ( 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) ) is one-to-one & (f : ( ( ) ( Relation-like the carrier of b2 : ( ( 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 ) Lattice) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( 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) : ( ( ) ( non empty ) set ) -valued Function-like non empty V19( the carrier of b2 : ( ( 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 ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) Homomorphism of b2 : ( ( 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 ) Lattice) ,b1 : ( ( 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) ) . i : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( 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) : ( ( ) ( non empty ) set ) ) "/\" (f : ( ( ) ( Relation-like the carrier of b2 : ( ( 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 ) Lattice) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( 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) : ( ( ) ( non empty ) set ) -valued Function-like non empty V19( the carrier of b2 : ( ( 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 ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) Homomorphism of b2 : ( ( 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 ) Lattice) ,b1 : ( ( 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) ) . k : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( 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) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( 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) : ( ( ) ( non empty ) set ) ) [= f : ( ( ) ( Relation-like the carrier of b2 : ( ( 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 ) Lattice) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( 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) : ( ( ) ( non empty ) set ) -valued Function-like non empty V19( the carrier of b2 : ( ( 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 ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) Homomorphism of b2 : ( ( 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 ) Lattice) ,b1 : ( ( 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) ) . j : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( 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) : ( ( ) ( non empty ) set ) ) holds
f : ( ( ) ( Relation-like the carrier of b2 : ( ( 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 ) Lattice) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( 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) : ( ( ) ( non empty ) set ) -valued Function-like non empty V19( the carrier of b2 : ( ( 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 ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) Homomorphism of b2 : ( ( 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 ) Lattice) ,b1 : ( ( 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) ) . k : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( 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) : ( ( ) ( non empty ) set ) ) [= f : ( ( ) ( Relation-like the carrier of b2 : ( ( 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 ) Lattice) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( 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) : ( ( ) ( non empty ) set ) -valued Function-like non empty V19( the carrier of b2 : ( ( 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 ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) Homomorphism of b2 : ( ( 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 ) Lattice) ,b1 : ( ( 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) ) . (i : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) => j : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( 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 ) Lattice) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( 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) : ( ( ) ( non empty ) set ) ) ;

theorem :: LATTICE4:28
for CL being ( ( 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)
for IL 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 ) Lattice)
for f being ( ( ) ( Relation-like the carrier of b2 : ( ( 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 ) Lattice) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( 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) : ( ( ) ( non empty ) set ) -valued Function-like non empty V19( the carrier of b2 : ( ( 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 ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) Homomorphism of IL : ( ( 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 ) Lattice) ,CL : ( ( 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) ) st f : ( ( ) ( Relation-like the carrier of b2 : ( ( 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 ) Lattice) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( 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) : ( ( ) ( non empty ) set ) -valued Function-like non empty V19( the carrier of b2 : ( ( 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 ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) Homomorphism of b2 : ( ( 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 ) Lattice) ,b1 : ( ( 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) ) is bijective holds
( CL : ( ( 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) is implicative & f : ( ( ) ( Relation-like the carrier of b2 : ( ( 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 ) Lattice) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( 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) : ( ( ) ( non empty ) set ) -valued Function-like non empty V19( the carrier of b2 : ( ( 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 ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) Homomorphism of b2 : ( ( 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 ) Lattice) ,b1 : ( ( 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) ) preserves_implication ) ;

begin

theorem :: LATTICE4:29
for BL 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 Heyting implicative ) Lattice) holds (Top BL : ( ( 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 Heyting implicative ) 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 Heyting implicative ) 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) ) = Bottom BL : ( ( 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 Heyting implicative ) 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) ) ;

theorem :: LATTICE4:30
for BL 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 Heyting implicative ) Lattice) holds (Bottom BL : ( ( 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 Heyting implicative ) 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 Heyting implicative ) 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) ) = Top BL : ( ( 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 Heyting implicative ) 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) ) ;

theorem :: LATTICE4:31
for CL being ( ( 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)
for BL 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 Heyting implicative ) Lattice)
for f being ( ( ) ( Relation-like the carrier of b2 : ( ( 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( 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) : ( ( ) ( non empty ) set ) -valued Function-like non empty V19( the carrier of b2 : ( ( 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) Homomorphism of BL : ( ( 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 Heyting implicative ) Lattice) ,CL : ( ( 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) ) st f : ( ( ) ( Relation-like the carrier of b2 : ( ( 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( 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) : ( ( ) ( non empty ) set ) -valued Function-like non empty V19( the carrier of b2 : ( ( 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) Homomorphism of b2 : ( ( 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 Heyting implicative ) Lattice) ,b1 : ( ( 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) ) is onto holds
( CL : ( ( 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) is Boolean & f : ( ( ) ( Relation-like the carrier of b2 : ( ( 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( 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) : ( ( ) ( non empty ) set ) -valued Function-like non empty V19( the carrier of b2 : ( ( 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) Homomorphism of b2 : ( ( 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 Heyting implicative ) Lattice) ,b1 : ( ( 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) ) preserves_complement ) ;

definition
let BL 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 Heyting implicative ) Lattice) ;
mode Field of BL -> ( ( non empty ) ( non empty ) Subset of ) means :: LATTICE4:def 9
 for a, b being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in it : ( ( ) ( ) set ) & b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in it : ( ( ) ( ) set ) holds
( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\" b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of BL : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) ) in it : ( ( ) ( ) set ) & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ` : ( ( ) ( ) Element of the carrier of BL : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) ) in it : ( ( ) ( ) set ) );
end;

theorem :: LATTICE4:32
for BL 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 Heyting implicative ) Lattice)
for a, b being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for F being ( ( ) ( non empty ) Field of BL : ( ( 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 Heyting implicative ) Lattice) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in F : ( ( ) ( non empty ) Field 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 Heyting implicative ) Lattice) ) & b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in F : ( ( ) ( non empty ) Field 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 Heyting implicative ) Lattice) ) holds
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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) ) in F : ( ( ) ( non empty ) Field 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 Heyting implicative ) Lattice) ) ;

theorem :: LATTICE4:33
for BL 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 Heyting implicative ) Lattice)
for a, b being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for F being ( ( ) ( non empty ) Field of BL : ( ( 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 Heyting implicative ) Lattice) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in F : ( ( ) ( non empty ) Field 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 Heyting implicative ) Lattice) ) & b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in F : ( ( ) ( non empty ) Field 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 Heyting implicative ) Lattice) ) holds
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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) ) in F : ( ( ) ( non empty ) Field 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 Heyting implicative ) Lattice) ) ;

theorem :: LATTICE4:34
for BL 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 Heyting implicative ) Lattice) holds the carrier of BL : ( ( 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) is ( ( ) ( non empty ) Field of BL : ( ( 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 Heyting implicative ) Lattice) ) ;

theorem :: LATTICE4:35
for BL 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 Heyting implicative ) Lattice)
for F being ( ( ) ( non empty ) Field of BL : ( ( 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 Heyting implicative ) Lattice) ) holds F : ( ( ) ( non empty ) Field 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 Heyting implicative ) Lattice) ) is ( ( meet-closed join-closed ) ( meet-closed join-closed ) ClosedSubset of BL : ( ( 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 Heyting implicative ) Lattice) ) ;

definition
let BL 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 Heyting implicative ) Lattice) ;
let A be ( ( non empty ) ( non empty ) Subset of ) ;
func field_by A -> ( ( ) ( non empty ) Field of BL : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) ) means :: LATTICE4:def 10
( A : ( ( ) ( ) set ) c= it : ( ( Function-like quasi_total ) ( Relation-like [:BL : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) ,BL : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) :] : ( ( ) ( ) set ) -defined BL : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) -valued Function-like quasi_total ) Element of bool [:[:BL : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) ,BL : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) :] : ( ( ) ( ) set ) ,BL : ( ( 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 ) ) & ( for F being ( ( ) ( non empty ) Field of BL : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) ) st A : ( ( ) ( ) set ) c= F : ( ( ) ( non empty ) Field of BL : ( ( 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 Heyting implicative ) Lattice) ) holds
it : ( ( Function-like quasi_total ) ( Relation-like [:BL : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) ,BL : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) :] : ( ( ) ( ) set ) -defined BL : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) -valued Function-like quasi_total ) Element of bool [:[:BL : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) ,BL : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) :] : ( ( ) ( ) set ) ,BL : ( ( 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 ) ) c= F : ( ( ) ( non empty ) Field of BL : ( ( 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 Heyting implicative ) Lattice) ) ) );
end;

definition
let BL 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 Heyting implicative ) Lattice) ;
let A be ( ( non empty ) ( non empty ) Subset of ) ;
func SetImp A -> ( ( ) ( ) Subset of ) equals :: LATTICE4:def 11
 { (a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) => b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of BL : ( ( 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 a, b is ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in A : ( ( ) ( ) set ) & b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in A : ( ( ) ( ) set ) ) } ;
end;

registration
let BL 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 Heyting implicative ) Lattice) ;
let A be ( ( non empty ) ( non empty ) Subset of ) ;
cluster SetImp A : ( ( non empty ) ( non empty ) Element of bool the carrier of BL : ( ( 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 Heyting implicative ) LattStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ) -> non empty ;
end;

theorem :: LATTICE4:36
for x being ( ( ) ( ) set )
for BL 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 Heyting implicative ) Lattice)
for A being ( ( non empty ) ( non empty ) Subset of ) holds
( x : ( ( ) ( ) set ) in SetImp A : ( ( non empty ) ( non empty ) Subset of ) : ( ( ) ( non empty ) Subset of ) iff 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 b2 : ( ( 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in A : ( ( non empty ) ( non empty ) Subset of ) & q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in A : ( ( non empty ) ( non empty ) Subset of ) ) ) ;

theorem :: LATTICE4:37
for BL 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 Heyting implicative ) Lattice)
for A being ( ( non empty ) ( non empty ) Subset of )
for c being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in SetImp A : ( ( non empty ) ( non empty ) Subset of ) : ( ( ) ( non empty ) Subset of ) iff ex p, q being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = (p : ( ( ) ( ) 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) ) "\/" q : ( ( ) ( ) 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) ) & p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in A : ( ( non empty ) ( non empty ) Subset of ) & q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in A : ( ( non empty ) ( non empty ) Subset of ) ) ) ;

definition
let BL 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 Heyting implicative ) Lattice) ;
func comp BL -> ( ( Function-like quasi_total ) ( Relation-like the carrier of BL : ( ( 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 BL : ( ( 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 non empty V19( the carrier of BL : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of the carrier of BL : ( ( 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 BL : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) ) means :: LATTICE4:def 12
 for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds it : ( ( ) ( ) set ) . a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of BL : ( ( non empty Lattice-like ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) ) = a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ` : ( ( ) ( ) Element of the carrier of BL : ( ( 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 :: LATTICE4:38
for BL 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 Heyting implicative ) Lattice)
for b being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for B being ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) holds FinJoin ((B : ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) \/ {.b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) .} : ( ( ) ( non empty ) Element of Fin 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) : ( ( preBoolean ) ( preBoolean ) set ) ) ) : ( ( ) ( non empty ) Element of Fin 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) : ( ( preBoolean ) ( preBoolean ) set ) ) ,(comp BL : ( ( 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 Heyting implicative ) Lattice) ) : ( ( Function-like quasi_total ) ( Relation-like 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) -defined 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) -valued Function-like non empty V19( 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) Function 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) , 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 Heyting implicative ) 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) ) = (FinJoin (B : ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) ,(comp BL : ( ( 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 Heyting implicative ) Lattice) ) : ( ( Function-like quasi_total ) ( Relation-like 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) -defined 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) -valued Function-like non empty V19( 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) Function 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) , 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 Heyting implicative ) 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 Heyting implicative ) 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 Heyting implicative ) 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) ) ;

theorem :: LATTICE4:39
for BL 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 Heyting implicative ) Lattice)
for B being ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) holds (FinJoin B : ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) ) : ( ( ) ( ) 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) ) = FinMeet (B : ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) ,(comp BL : ( ( 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 Heyting implicative ) Lattice) ) : ( ( Function-like quasi_total ) ( Relation-like 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) -defined 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) -valued Function-like non empty V19( 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) Function 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) , 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 Heyting implicative ) 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) ) ;

theorem :: LATTICE4:40
for BL 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 Heyting implicative ) Lattice)
for b being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for B being ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) holds FinMeet ((B : ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) \/ {.b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) .} : ( ( ) ( non empty ) Element of Fin 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) : ( ( preBoolean ) ( preBoolean ) set ) ) ) : ( ( ) ( non empty ) Element of Fin 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) : ( ( preBoolean ) ( preBoolean ) set ) ) ,(comp BL : ( ( 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 Heyting implicative ) Lattice) ) : ( ( Function-like quasi_total ) ( Relation-like 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) -defined 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) -valued Function-like non empty V19( 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) Function 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) , 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 Heyting implicative ) 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) ) = (FinMeet (B : ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) ,(comp BL : ( ( 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 Heyting implicative ) Lattice) ) : ( ( Function-like quasi_total ) ( Relation-like 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) -defined 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) -valued Function-like non empty V19( 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) Function 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) , 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 Heyting implicative ) 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 Heyting implicative ) 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 Heyting implicative ) 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) ) ;

theorem :: LATTICE4:41
for BL 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 Heyting implicative ) Lattice)
for B being ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) holds (FinMeet B : ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) ) : ( ( ) ( ) 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) ) = FinJoin (B : ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) ,(comp BL : ( ( 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 Heyting implicative ) Lattice) ) : ( ( Function-like quasi_total ) ( Relation-like 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) -defined 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) -valued Function-like non empty V19( 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) Function 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) , 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 Heyting implicative ) 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) ) ;

theorem :: LATTICE4:42
for BL 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 Heyting implicative ) Lattice)
for AF being ( ( non empty meet-closed join-closed ) ( non empty meet-closed join-closed ) ClosedSubset of BL : ( ( 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 Heyting implicative ) Lattice) ) st Bottom BL : ( ( 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 Heyting implicative ) 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) ) in AF : ( ( non empty meet-closed join-closed ) ( non empty meet-closed join-closed ) ClosedSubset 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 Heyting implicative ) Lattice) ) & Top BL : ( ( 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 Heyting implicative ) 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) ) in AF : ( ( non empty meet-closed join-closed ) ( non empty meet-closed join-closed ) ClosedSubset 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 Heyting implicative ) Lattice) ) holds
for B being ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) st B : ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) c= SetImp AF : ( ( non empty meet-closed join-closed ) ( non empty meet-closed join-closed ) ClosedSubset 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 Heyting implicative ) Lattice) ) : ( ( ) ( non empty ) Subset of ) holds
ex B0 being ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) st
( B0 : ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) c= SetImp AF : ( ( non empty meet-closed join-closed ) ( non empty meet-closed join-closed ) ClosedSubset 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 Heyting implicative ) Lattice) ) : ( ( ) ( non empty ) Subset of ) & FinJoin (B : ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) ,(comp BL : ( ( 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 Heyting implicative ) Lattice) ) : ( ( Function-like quasi_total ) ( Relation-like 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) -defined 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) -valued Function-like non empty V19( 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) ) quasi_total ) Function 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) , 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 Heyting implicative ) 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) ) = FinMeet B0 : ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ;

theorem :: LATTICE4:43
for BL 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 Heyting implicative ) Lattice)
for AF being ( ( non empty meet-closed join-closed ) ( non empty meet-closed join-closed ) ClosedSubset of BL : ( ( 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 Heyting implicative ) Lattice) ) st Bottom BL : ( ( 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 Heyting implicative ) 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) ) in AF : ( ( non empty meet-closed join-closed ) ( non empty meet-closed join-closed ) ClosedSubset 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 Heyting implicative ) Lattice) ) & Top BL : ( ( 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 Heyting implicative ) 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 Heyting implicative ) Lattice) : ( ( ) ( non empty ) set ) ) in AF : ( ( non empty meet-closed join-closed ) ( non empty meet-closed join-closed ) ClosedSubset 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 Heyting implicative ) Lattice) ) holds
{ (FinMeet B : ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) where B is ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) : B : ( ( ) ( ) Finite_Subset of ( ( preBoolean ) ( preBoolean ) set ) ) c= SetImp AF : ( ( non empty meet-closed join-closed ) ( non empty meet-closed join-closed ) ClosedSubset 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 Heyting implicative ) Lattice) ) : ( ( ) ( non empty ) Subset of ) } = field_by AF : ( ( non empty meet-closed join-closed ) ( non empty meet-closed join-closed ) ClosedSubset 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 Heyting implicative ) Lattice) ) : ( ( ) ( non empty ) Field 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 Heyting implicative ) Lattice) ) ;