:: WAYBEL15 semantic presentation

begin

theorem :: WAYBEL15:1
for R being ( ( ) ( ) RelStr )
for S being ( ( full ) ( full ) SubRelStr of R : ( ( ) ( ) RelStr ) )
for T being ( ( full ) ( full ) SubRelStr of S : ( ( full ) ( full ) SubRelStr of b1 : ( ( ) ( ) RelStr ) ) ) holds T : ( ( full ) ( full ) SubRelStr of b2 : ( ( full ) ( full ) SubRelStr of b1 : ( ( ) ( ) RelStr ) ) ) is ( ( full ) ( full ) SubRelStr of R : ( ( ) ( ) RelStr ) ) ;

theorem :: WAYBEL15:2
for X being ( ( ) ( ) set )
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds uparrow a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty filtered upper ) Element of K32( the carrier of (BoolePoset b1 : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = { Y : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) where Y is ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) c= Y : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) } ;

theorem :: WAYBEL15:3
for L being ( ( non empty antisymmetric upper-bounded ) ( non empty antisymmetric upper-bounded ) RelStr )
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st Top L : ( ( non empty antisymmetric upper-bounded ) ( non empty antisymmetric upper-bounded ) RelStr ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty antisymmetric upper-bounded ) ( non empty antisymmetric upper-bounded ) RelStr ) : ( ( ) ( non empty ) set ) ) <= a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = Top L : ( ( non empty antisymmetric upper-bounded ) ( non empty antisymmetric upper-bounded ) RelStr ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty antisymmetric upper-bounded ) ( non empty antisymmetric upper-bounded ) RelStr ) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL15:4
for S, T being ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset)
for g being ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) V11( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for d being ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) V11( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st g : ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) V11( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is onto & [g : ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) V11( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ,d : ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) V11( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ] : ( ( ) ( ) Connection of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) ,b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) ) is Galois holds
T : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) , Image d : ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) V11( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( strict full ) ( non empty strict reflexive transitive antisymmetric full ) SubRelStr of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) ) are_isomorphic ;

theorem :: WAYBEL15:5
for L1, L2, L3 being ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset)
for g1 being ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) V11( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for g2 being ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) V11( the carrier of b3 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for d1 being ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) V11( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for d2 being ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b3 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) V11( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b3 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st [g1 : ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) V11( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ,d1 : ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) V11( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ] : ( ( ) ( ) Connection of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) ,b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) ) is Galois & [g2 : ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) V11( the carrier of b3 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ,d2 : ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b3 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) V11( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b3 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ] : ( ( ) ( ) Connection of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) ,b3 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) ) is Galois holds
[(g2 : ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) V11( the carrier of b3 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) * g1 : ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) V11( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( non empty V7() V10( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) V11( the carrier of b3 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of K32(K33( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) , the carrier of b3 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,(d1 : ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) V11( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) * d2 : ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b3 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) V11( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b3 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( Function-like ) ( non empty V7() V10( the carrier of b3 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) V11( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b3 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of K32(K33( the carrier of b3 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ] : ( ( ) ( ) Connection of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) ,b3 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) ) is Galois ;

theorem :: WAYBEL15:6
for L1, L2 being ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset)
for f being ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) V11( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for f1 being ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) V11( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f1 : ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) V11( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) = f : ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) V11( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) " : ( ( V7() Function-like ) ( V7() Function-like ) set ) & f : ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) V11( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is isomorphic holds
( [f : ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) V11( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ,f1 : ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) V11( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ] : ( ( ) ( ) Connection of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) ,b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) ) is Galois & [f1 : ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) V11( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ,f : ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) V11( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ] : ( ( ) ( ) Connection of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) ,b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) ) is Galois ) ;

theorem :: WAYBEL15:7
for X being ( ( ) ( ) set ) holds BoolePoset X : ( ( ) ( ) set ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) is arithmetic ;

registration
let X be ( ( ) ( ) set ) ;
cluster BoolePoset X : ( ( ) ( ) set ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) -> strict arithmetic ;
end;

theorem :: WAYBEL15:8
for L1, L2 being ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) Poset)
for f being ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) Poset) : ( ( ) ( non empty ) set ) ) V11( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) Poset) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) Poset) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) Poset) : ( ( ) ( non empty ) set ) ) V11( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) Poset) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) Poset) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is isomorphic holds
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds f : ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) Poset) : ( ( ) ( non empty ) set ) ) V11( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) Poset) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) Poset) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) .: (waybelow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( lower ) Element of K32( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) Poset) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K32( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) Poset) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = waybelow (f : ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) Poset) : ( ( ) ( non empty ) set ) ) V11( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) Poset) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) Poset) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) Poset) : ( ( ) ( non empty ) set ) ) : ( ( ) ( lower ) Element of K32( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) Poset) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL15:9
for L1, L2 being ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) st L1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) ,L2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) are_isomorphic & L1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) is continuous holds
L2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) is continuous ;

theorem :: WAYBEL15:10
for L1, L2 being ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric with_suprema with_infima ) LATTICE) st L1 : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric with_suprema with_infima ) LATTICE) ,L2 : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric with_suprema with_infima ) LATTICE) are_isomorphic & L1 : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric with_suprema with_infima ) LATTICE) is lower-bounded & L1 : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric with_suprema with_infima ) LATTICE) is arithmetic holds
L2 : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric with_suprema with_infima ) LATTICE) is arithmetic ;

theorem :: WAYBEL15:11
for L1, L2, L3 being ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset)
for f being ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) V11( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for g being ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) V11( the carrier of b3 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st f : ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) V11( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is directed-sups-preserving & g : ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) V11( the carrier of b3 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is directed-sups-preserving holds
g : ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) V11( the carrier of b3 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) * f : ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) V11( the carrier of b2 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( Function-like ) ( non empty V7() V10( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) V11( the carrier of b3 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) quasi_total ) Element of K32(K33( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) , the carrier of b3 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) is directed-sups-preserving ;

begin

theorem :: WAYBEL15:12
for L1, L2 being ( ( non empty ) ( non empty ) RelStr )
for f being ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) V11( the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) )
for X being ( ( ) ( ) Subset of ) holds (inclusion f : ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) V11( the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of (Image b3 : ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) V11( the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( strict full ) ( non empty strict full ) SubRelStr of b2 : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( ) ( non empty ) set ) ) V11( the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) Function-like one-to-one V27( the carrier of (Image b3 : ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) V11( the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( strict full ) ( non empty strict full ) SubRelStr of b2 : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( ) ( non empty ) set ) ) quasi_total monotone ) Element of K32(K33( the carrier of (Image b3 : ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) V11( the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( strict full ) ( non empty strict full ) SubRelStr of b2 : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) .: X : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K32( the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = X : ( ( ) ( ) Subset of ) ;

theorem :: WAYBEL15:13
for X being ( ( ) ( ) set )
for c being ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of (BoolePoset b1 : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) : ( ( ) ( non empty ) set ) ) V11( the carrier of (BoolePoset b1 : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of (BoolePoset b1 : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st c : ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of (BoolePoset b1 : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) : ( ( ) ( non empty ) set ) ) V11( the carrier of (BoolePoset b1 : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of (BoolePoset b1 : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is idempotent & c : ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of (BoolePoset b1 : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) : ( ( ) ( non empty ) set ) ) V11( the carrier of (BoolePoset b1 : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of (BoolePoset b1 : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is directed-sups-preserving holds
inclusion c : ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of (BoolePoset b1 : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) : ( ( ) ( non empty ) set ) ) V11( the carrier of (BoolePoset b1 : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of (BoolePoset b1 : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of (Image b2 : ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of (BoolePoset b1 : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) : ( ( ) ( non empty ) set ) ) V11( the carrier of (BoolePoset b1 : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of (BoolePoset b1 : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( strict full ) ( non empty strict reflexive transitive antisymmetric full ) SubRelStr of BoolePoset b1 : ( ( ) ( ) set ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) ) : ( ( ) ( non empty ) set ) ) V11( the carrier of (BoolePoset b1 : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) : ( ( ) ( non empty ) set ) ) Function-like one-to-one V27( the carrier of (Image b2 : ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of (BoolePoset b1 : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) : ( ( ) ( non empty ) set ) ) V11( the carrier of (BoolePoset b1 : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of (BoolePoset b1 : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( strict full ) ( non empty strict reflexive transitive antisymmetric full ) SubRelStr of BoolePoset b1 : ( ( ) ( ) set ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) ) : ( ( ) ( non empty ) set ) ) quasi_total monotone ) Element of K32(K33( the carrier of (Image b2 : ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of (BoolePoset b1 : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) : ( ( ) ( non empty ) set ) ) V11( the carrier of (BoolePoset b1 : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of (BoolePoset b1 : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( strict full ) ( non empty strict reflexive transitive antisymmetric full ) SubRelStr of BoolePoset b1 : ( ( ) ( ) set ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) ) : ( ( ) ( non empty ) set ) , the carrier of (BoolePoset b1 : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) is directed-sups-preserving ;

theorem :: WAYBEL15:14
for L being ( ( reflexive transitive antisymmetric with_suprema with_infima complete continuous ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous ) LATTICE)
for p being ( ( Function-like quasi_total kernel ) ( non empty V7() V10( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete continuous ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) ) V11( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete continuous ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete continuous ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) ) quasi_total idempotent monotone projection kernel ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st p : ( ( Function-like quasi_total kernel ) ( non empty V7() V10( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete continuous ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) ) V11( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete continuous ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete continuous ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) ) quasi_total idempotent monotone projection kernel ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is directed-sups-preserving holds
Image p : ( ( Function-like quasi_total kernel ) ( non empty V7() V10( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete continuous ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) ) V11( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete continuous ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete continuous ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) ) quasi_total idempotent monotone projection kernel ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( strict full ) ( non empty strict reflexive transitive antisymmetric full ) SubRelStr of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete continuous ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous ) LATTICE) ) is ( ( reflexive transitive antisymmetric with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous ) LATTICE) ;

theorem :: WAYBEL15:15
for L being ( ( reflexive transitive antisymmetric with_suprema with_infima complete continuous ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous ) LATTICE)
for p being ( ( Function-like quasi_total projection ) ( non empty V7() V10( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete continuous ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) ) V11( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete continuous ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete continuous ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) ) quasi_total idempotent monotone projection ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st p : ( ( Function-like quasi_total projection ) ( non empty V7() V10( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete continuous ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) ) V11( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete continuous ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete continuous ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) ) quasi_total idempotent monotone projection ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is directed-sups-preserving holds
Image p : ( ( Function-like quasi_total projection ) ( non empty V7() V10( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete continuous ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) ) V11( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete continuous ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete continuous ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous ) LATTICE) : ( ( ) ( non empty ) set ) ) quasi_total idempotent monotone projection ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( strict full ) ( non empty strict reflexive transitive antisymmetric full ) SubRelStr of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete continuous ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous ) LATTICE) ) is ( ( reflexive transitive antisymmetric with_suprema with_infima continuous ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous ) LATTICE) ;

theorem :: WAYBEL15:16
for L being ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded ) LATTICE) holds
( L : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded ) LATTICE) is continuous iff ex A being ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded arithmetic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) LATTICE) ex g being ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b2 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded arithmetic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) LATTICE) : ( ( ) ( non empty ) set ) ) V11( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded ) LATTICE) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b2 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded arithmetic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) LATTICE) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st
( g : ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b2 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded arithmetic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) LATTICE) : ( ( ) ( non empty ) set ) ) V11( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded ) LATTICE) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b2 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded arithmetic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) LATTICE) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is onto & g : ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b2 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded arithmetic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) LATTICE) : ( ( ) ( non empty ) set ) ) V11( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded ) LATTICE) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b2 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded arithmetic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) LATTICE) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is infs-preserving & g : ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b2 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded arithmetic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) LATTICE) : ( ( ) ( non empty ) set ) ) V11( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded ) LATTICE) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b2 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded arithmetic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) LATTICE) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is directed-sups-preserving ) ) ;

theorem :: WAYBEL15:17
for L being ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded ) LATTICE) holds
( L : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded ) LATTICE) is continuous iff ex A being ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) ex g being ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b2 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) V11( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded ) LATTICE) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b2 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st
( g : ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b2 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) V11( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded ) LATTICE) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b2 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is onto & g : ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b2 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) V11( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded ) LATTICE) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b2 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is infs-preserving & g : ( ( Function-like quasi_total ) ( non empty V7() V10( the carrier of b2 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) V11( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded ) LATTICE) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of b2 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is directed-sups-preserving ) ) ;

theorem :: WAYBEL15:18
for L being ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded ) LATTICE) holds
( ( L : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded ) LATTICE) is continuous implies ex X being ( ( non empty ) ( non empty ) set ) ex p being ( ( Function-like quasi_total projection ) ( non empty V7() V10( the carrier of (BoolePoset b2 : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) : ( ( ) ( non empty ) set ) ) V11( the carrier of (BoolePoset b2 : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of (BoolePoset b2 : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total idempotent monotone projection ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st
( p : ( ( Function-like quasi_total projection ) ( non empty V7() V10( the carrier of (BoolePoset b2 : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) : ( ( ) ( non empty ) set ) ) V11( the carrier of (BoolePoset b2 : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of (BoolePoset b2 : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total idempotent monotone projection ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is directed-sups-preserving & L : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded ) LATTICE) , Image p : ( ( Function-like quasi_total projection ) ( non empty V7() V10( the carrier of (BoolePoset b2 : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) : ( ( ) ( non empty ) set ) ) V11( the carrier of (BoolePoset b2 : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of (BoolePoset b2 : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total idempotent monotone projection ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( strict full ) ( non empty strict reflexive transitive antisymmetric full ) SubRelStr of BoolePoset b2 : ( ( ) ( ) set ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) ) are_isomorphic ) ) & ( ex X being ( ( ) ( ) set ) ex p being ( ( Function-like quasi_total projection ) ( non empty V7() V10( the carrier of (BoolePoset b2 : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) : ( ( ) ( non empty ) set ) ) V11( the carrier of (BoolePoset b2 : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of (BoolePoset b2 : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total idempotent monotone projection ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st
( p : ( ( Function-like quasi_total projection ) ( non empty V7() V10( the carrier of (BoolePoset b2 : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) : ( ( ) ( non empty ) set ) ) V11( the carrier of (BoolePoset b2 : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of (BoolePoset b2 : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total idempotent monotone projection ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is directed-sups-preserving & L : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded ) LATTICE) , Image p : ( ( Function-like quasi_total projection ) ( non empty V7() V10( the carrier of (BoolePoset b2 : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) : ( ( ) ( non empty ) set ) ) V11( the carrier of (BoolePoset b2 : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) : ( ( ) ( non empty ) set ) ) Function-like V27( the carrier of (BoolePoset b2 : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total idempotent monotone projection ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( strict full ) ( non empty strict reflexive transitive antisymmetric full ) SubRelStr of BoolePoset b2 : ( ( ) ( ) set ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) ) are_isomorphic ) implies L : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded ) LATTICE) is continuous ) ) ;

begin

theorem :: WAYBEL15:19
for L being ( ( non empty ) ( non empty ) RelStr )
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in PRIME (L : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( ) Element of K32( the carrier of (b1 : ( ( non empty ) ( non empty ) RelStr ) opp) : ( ( strict ) ( non empty strict ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) iff x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is co-prime ) ;

definition
let L be ( ( non empty ) ( non empty ) RelStr ) ;
let a be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
attr a is atom means :: WAYBEL15:def 1
( Bottom L : ( ( V5() ) ( V5() ) set ) : ( ( ) ( ) Element of the carrier of L : ( ( V5() ) ( V5() ) set ) : ( ( ) ( ) set ) ) < a : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) & ( for b being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st Bottom L : ( ( V5() ) ( V5() ) set ) : ( ( ) ( ) Element of the carrier of L : ( ( V5() ) ( V5() ) set ) : ( ( ) ( ) set ) ) < b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= a : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) holds
b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = a : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) );
end;

definition
let L be ( ( non empty ) ( non empty ) RelStr ) ;
func ATOM L -> ( ( ) ( ) Subset of ) means :: WAYBEL15:def 2
 for x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in it : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) iff x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is atom );
end;

theorem :: WAYBEL15:20
for L being ( ( reflexive transitive antisymmetric with_suprema with_infima Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V226() distributive V266() complemented Boolean ) LATTICE)
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is atom iff ( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is co-prime & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> Bottom L : ( ( reflexive transitive antisymmetric with_suprema with_infima Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V226() distributive V266() complemented Boolean ) LATTICE) : ( ( ) ( ) Element of the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V226() distributive V266() complemented Boolean ) LATTICE) : ( ( ) ( non empty ) set ) ) ) ) ;

registration
let L be ( ( reflexive transitive antisymmetric with_suprema with_infima Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V226() distributive V266() complemented Boolean ) LATTICE) ;
cluster atom -> co-prime for ( ( ) ( ) Element of the carrier of L : ( ( V5() ) ( V5() ) set ) : ( ( ) ( ) set ) ) ;
end;

theorem :: WAYBEL15:21
for L being ( ( reflexive transitive antisymmetric with_suprema with_infima Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V226() distributive V266() complemented Boolean ) LATTICE) holds ATOM L : ( ( reflexive transitive antisymmetric with_suprema with_infima Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V226() distributive V266() complemented Boolean ) LATTICE) : ( ( ) ( ) Subset of ) = (PRIME (L : ( ( reflexive transitive antisymmetric with_suprema with_infima Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V226() distributive V266() complemented Boolean ) LATTICE) opp) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric ) RelStr ) ) : ( ( ) ( ) Element of K32( the carrier of (b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V226() distributive V266() complemented Boolean ) LATTICE) opp) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) \ {(Bottom L : ( ( reflexive transitive antisymmetric with_suprema with_infima Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V226() distributive V266() complemented Boolean ) LATTICE) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V226() distributive V266() complemented Boolean ) LATTICE) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty finite ) Element of K32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V226() distributive V266() complemented Boolean ) LATTICE) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K32( the carrier of (b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V226() distributive V266() complemented Boolean ) LATTICE) opp) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL15:22
for L being ( ( reflexive transitive antisymmetric with_suprema with_infima Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V226() distributive V266() complemented Boolean ) LATTICE)
for x, a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is atom holds
( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) iff not a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= 'not' x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V226() distributive V266() complemented Boolean ) LATTICE) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: WAYBEL15:23
for L being ( ( reflexive transitive antisymmetric with_suprema with_infima complete Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean ) LATTICE)
for X being ( ( ) ( ) Subset of )
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\" (sup X : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean ) LATTICE) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean ) LATTICE) : ( ( ) ( non empty ) set ) ) = "\/" ( { (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\" y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean ) LATTICE) : ( ( ) ( non empty ) set ) ) where y is ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in X : ( ( ) ( ) Subset of ) } ,L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean ) LATTICE) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean ) LATTICE) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL15:24
for L being ( ( non empty antisymmetric with_infima lower-bounded ) ( non empty antisymmetric with_infima lower-bounded ) RelStr )
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is atom & y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is atom & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\" y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty antisymmetric with_infima lower-bounded ) ( non empty antisymmetric with_infima lower-bounded ) RelStr ) : ( ( ) ( non empty ) set ) ) = Bottom L : ( ( non empty antisymmetric with_infima lower-bounded ) ( non empty antisymmetric with_infima lower-bounded ) RelStr ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty antisymmetric with_infima lower-bounded ) ( non empty antisymmetric with_infima lower-bounded ) RelStr ) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL15:25
for L being ( ( reflexive transitive antisymmetric with_suprema with_infima complete Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean ) LATTICE)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) c= ATOM L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean ) LATTICE) : ( ( ) ( ) Subset of ) holds
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in A : ( ( ) ( ) Subset of ) iff ( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is atom & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= sup A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean ) LATTICE) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: WAYBEL15:26
for L being ( ( reflexive transitive antisymmetric with_suprema with_infima complete Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean ) LATTICE)
for X, Y being ( ( ) ( ) Subset of ) st X : ( ( ) ( ) Subset of ) c= ATOM L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean ) LATTICE) : ( ( ) ( ) Subset of ) & Y : ( ( ) ( ) Subset of ) c= ATOM L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean ) LATTICE) : ( ( ) ( ) Subset of ) holds
( X : ( ( ) ( ) Subset of ) c= Y : ( ( ) ( ) Subset of ) iff sup X : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean ) LATTICE) : ( ( ) ( non empty ) set ) ) <= sup Y : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean ) LATTICE) : ( ( ) ( non empty ) set ) ) ) ;

begin

theorem :: WAYBEL15:27
for L being ( ( reflexive transitive antisymmetric with_suprema with_infima Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V226() distributive V266() complemented Boolean ) LATTICE) holds
( L : ( ( reflexive transitive antisymmetric with_suprema with_infima Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V226() distributive V266() complemented Boolean ) LATTICE) is arithmetic iff ex X being ( ( ) ( ) set ) st L : ( ( reflexive transitive antisymmetric with_suprema with_infima Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V226() distributive V266() complemented Boolean ) LATTICE) , BoolePoset X : ( ( ) ( ) set ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) are_isomorphic ) ;

theorem :: WAYBEL15:28
for L being ( ( reflexive transitive antisymmetric with_suprema with_infima Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V226() distributive V266() complemented Boolean ) LATTICE) holds
( L : ( ( reflexive transitive antisymmetric with_suprema with_infima Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V226() distributive V266() complemented Boolean ) LATTICE) is arithmetic iff L : ( ( reflexive transitive antisymmetric with_suprema with_infima Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V226() distributive V266() complemented Boolean ) LATTICE) is algebraic ) ;

theorem :: WAYBEL15:29
for L being ( ( reflexive transitive antisymmetric with_suprema with_infima Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V226() distributive V266() complemented Boolean ) LATTICE) holds
( L : ( ( reflexive transitive antisymmetric with_suprema with_infima Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V226() distributive V266() complemented Boolean ) LATTICE) is arithmetic iff L : ( ( reflexive transitive antisymmetric with_suprema with_infima Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V226() distributive V266() complemented Boolean ) LATTICE) is continuous ) ;

theorem :: WAYBEL15:30
for L being ( ( reflexive transitive antisymmetric with_suprema with_infima Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V226() distributive V266() complemented Boolean ) LATTICE) holds
( L : ( ( reflexive transitive antisymmetric with_suprema with_infima Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V226() distributive V266() complemented Boolean ) LATTICE) is arithmetic iff ( L : ( ( reflexive transitive antisymmetric with_suprema with_infima Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V226() distributive V266() complemented Boolean ) LATTICE) is continuous & L : ( ( reflexive transitive antisymmetric with_suprema with_infima Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V226() distributive V266() complemented Boolean ) LATTICE) opp : ( ( strict ) ( non empty strict reflexive transitive antisymmetric ) RelStr ) is continuous ) ) ;

theorem :: WAYBEL15:31
for L being ( ( reflexive transitive antisymmetric with_suprema with_infima Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V226() distributive V266() complemented Boolean ) LATTICE) holds
( L : ( ( reflexive transitive antisymmetric with_suprema with_infima Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V226() distributive V266() complemented Boolean ) LATTICE) is arithmetic iff L : ( ( reflexive transitive antisymmetric with_suprema with_infima Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V226() distributive V266() complemented Boolean ) LATTICE) is completely-distributive ) ;

theorem :: WAYBEL15:32
for L being ( ( reflexive transitive antisymmetric with_suprema with_infima Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V226() distributive V266() complemented Boolean ) LATTICE) holds
( L : ( ( reflexive transitive antisymmetric with_suprema with_infima Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V226() distributive V266() complemented Boolean ) LATTICE) is arithmetic iff ( L : ( ( reflexive transitive antisymmetric with_suprema with_infima Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V226() distributive V266() complemented Boolean ) LATTICE) is complete & ( for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ex X being ( ( ) ( ) Subset of ) st
( X : ( ( ) ( ) Subset of ) c= ATOM L : ( ( reflexive transitive antisymmetric with_suprema with_infima Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V226() distributive V266() complemented Boolean ) LATTICE) : ( ( ) ( ) Subset of ) & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = sup X : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima Boolean ) ( non empty reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V226() distributive V266() complemented Boolean ) LATTICE) : ( ( ) ( non empty ) set ) ) ) ) ) ) ;