:: WAYBEL16 semantic presentation

begin

theorem :: WAYBEL16:1
for L being ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) sup-Semilattice)
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds "/\" (((uparrow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty filtered upper ) Element of K32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) sup-Semilattice) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) /\ (uparrow y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty filtered upper ) Element of K32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) sup-Semilattice) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) sup-Semilattice) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,L : ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) sup-Semilattice) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) sup-Semilattice) : ( ( ) ( 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 ) ( non empty reflexive transitive antisymmetric with_suprema ) sup-Semilattice) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL16:2
for L being ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima ) Semilattice)
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds "\/" (((downarrow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty directed lower ) Element of K32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima ) Semilattice) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) /\ (downarrow y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty directed lower ) Element of K32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima ) Semilattice) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima ) Semilattice) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,L : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima ) Semilattice) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima ) Semilattice) : ( ( ) ( 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_infima ) ( non empty reflexive transitive antisymmetric with_infima ) Semilattice) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL16:3
for L being ( ( non empty ) ( non empty ) RelStr )
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is_maximal_in the carrier of L : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) \ (uparrow y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K32( the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K32( the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) holds
(uparrow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K32( the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) \ {x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty finite ) Element of K32( the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K32( the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = (uparrow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K32( the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) /\ (uparrow y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K32( the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K32( the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL16:4
for L being ( ( non empty ) ( non empty ) RelStr )
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is_minimal_in the carrier of L : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) \ (downarrow y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K32( the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K32( the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) holds
(downarrow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K32( the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) \ {x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty finite ) Element of K32( the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K32( the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = (downarrow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K32( the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) /\ (downarrow y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K32( the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K32( the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL16:5
for L being ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) Poset)
for X, Y being ( ( ) ( ) Subset of )
for X9, Y9 being ( ( ) ( ) Subset of ) st X : ( ( ) ( ) Subset of ) = X9 : ( ( ) ( ) Subset of ) & Y : ( ( ) ( ) Subset of ) = Y9 : ( ( ) ( ) Subset of ) holds
X : ( ( ) ( ) Subset of ) "\/" Y : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) Poset) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = X9 : ( ( ) ( ) Subset of ) "/\" Y9 : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K32( the carrier of (b1 : ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) Poset) opp) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_infima ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL16:6
for L being ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima ) Poset)
for X, Y being ( ( ) ( ) Subset of )
for X9, Y9 being ( ( ) ( ) Subset of ) st X : ( ( ) ( ) Subset of ) = X9 : ( ( ) ( ) Subset of ) & Y : ( ( ) ( ) Subset of ) = Y9 : ( ( ) ( ) Subset of ) holds
X : ( ( ) ( ) Subset of ) "/\" Y : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima ) Poset) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = X9 : ( ( ) ( ) Subset of ) "\/" Y9 : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K32( the carrier of (b1 : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima ) Poset) opp) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL16:7
for L being ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) holds Filt L : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) : ( ( ) ( ) set ) = Ids (L : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) opp) : ( ( strict ) ( non empty strict reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) ;

theorem :: WAYBEL16:8
for L being ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) holds Ids L : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) = Filt (L : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) opp) : ( ( strict ) ( non empty strict reflexive transitive ) RelStr ) : ( ( ) ( ) set ) ;

begin

definition
let S, T be ( ( non empty reflexive transitive antisymmetric complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete ) Poset) ;
mode CLHomomorphism of S,T -> ( ( V12() V18( the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the carrier of T : ( ( ) ( ) NetStr over S : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) set ) ) ) ( V7() V10( the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) V11( the carrier of T : ( ( ) ( ) NetStr over S : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) set ) ) V12() V18( the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the carrier of T : ( ( ) ( ) NetStr over S : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( ) set ) ) means :: WAYBEL16:def 1
( it : ( ( ) ( V7() V10(T : ( ( ) ( ) NetStr over S : ( ( ) ( ) 1-sorted ) ) ) V11(T : ( ( ) ( ) NetStr over S : ( ( ) ( ) 1-sorted ) ) ) ) Element of K32(K33(T : ( ( ) ( ) NetStr over S : ( ( ) ( ) 1-sorted ) ) ,T : ( ( ) ( ) NetStr over S : ( ( ) ( ) 1-sorted ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) is directed-sups-preserving & it : ( ( ) ( V7() V10(T : ( ( ) ( ) NetStr over S : ( ( ) ( ) 1-sorted ) ) ) V11(T : ( ( ) ( ) NetStr over S : ( ( ) ( ) 1-sorted ) ) ) ) Element of K32(K33(T : ( ( ) ( ) NetStr over S : ( ( ) ( ) 1-sorted ) ) ,T : ( ( ) ( ) NetStr over S : ( ( ) ( ) 1-sorted ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) is infs-preserving );
end;

definition
let S be ( ( non empty reflexive transitive antisymmetric complete continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) Poset) ;
let A be ( ( ) ( ) Subset of ) ;
pred A is_FG_set means :: WAYBEL16:def 2
 for T being ( ( non empty reflexive transitive antisymmetric complete continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) Poset)
for f being ( ( V12() V18(A : ( ( ) ( ) NetStr over S : ( ( ) ( ) 1-sorted ) ) , the carrier of b1 : ( ( non empty reflexive transitive antisymmetric complete continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) Poset) : ( ( ) ( non empty ) set ) ) ) ( V7() V10(A : ( ( ) ( ) NetStr over S : ( ( ) ( ) 1-sorted ) ) ) V11( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric complete continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) Poset) : ( ( ) ( non empty ) set ) ) V12() V18(A : ( ( ) ( ) NetStr over S : ( ( ) ( ) 1-sorted ) ) , the carrier of b1 : ( ( non empty reflexive transitive antisymmetric complete continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) Poset) : ( ( ) ( non empty ) set ) ) ) Function of A : ( ( ) ( ) NetStr over S : ( ( ) ( ) 1-sorted ) ) , the carrier of T : ( ( non empty reflexive transitive antisymmetric complete continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) Poset) : ( ( ) ( non empty ) set ) ) ex h being ( ( ) ( V7() V10( the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) V11( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric complete continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) Poset) : ( ( ) ( non empty ) set ) ) V12() V18( the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty reflexive transitive antisymmetric complete continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) Poset) : ( ( ) ( non empty ) set ) ) ) CLHomomorphism of S : ( ( ) ( ) 1-sorted ) ,T : ( ( non empty reflexive transitive antisymmetric complete continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) Poset) ) st
( h : ( ( ) ( V7() V10( the carrier of S : ( ( non empty reflexive transitive antisymmetric complete continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) Poset) : ( ( ) ( non empty ) set ) ) V11( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric complete continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) Poset) : ( ( ) ( non empty ) set ) ) V12() V18( the carrier of S : ( ( non empty reflexive transitive antisymmetric complete continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) Poset) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty reflexive transitive antisymmetric complete continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) Poset) : ( ( ) ( non empty ) set ) ) ) CLHomomorphism of S : ( ( non empty reflexive transitive antisymmetric complete continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) Poset) ,b1 : ( ( non empty reflexive transitive antisymmetric complete continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) Poset) ) | A : ( ( ) ( ) NetStr over S : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( V7() V10( the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) V11( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric complete continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) Poset) : ( ( ) ( non empty ) set ) ) ) Element of K32(K33( the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty reflexive transitive antisymmetric complete continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) Poset) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) = f : ( ( V12() V18(A : ( ( ) ( ) Subset of ) , the carrier of b1 : ( ( non empty reflexive transitive antisymmetric complete continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) Poset) : ( ( ) ( non empty ) set ) ) ) ( V7() V10(A : ( ( ) ( ) Subset of ) ) V11( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric complete continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) Poset) : ( ( ) ( non empty ) set ) ) V12() V18(A : ( ( ) ( ) Subset of ) , the carrier of b1 : ( ( non empty reflexive transitive antisymmetric complete continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) Poset) : ( ( ) ( non empty ) set ) ) ) Function of A : ( ( ) ( ) Subset of ) , the carrier of b1 : ( ( non empty reflexive transitive antisymmetric complete continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) Poset) : ( ( ) ( non empty ) set ) ) & ( for h9 being ( ( ) ( V7() V10( the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) V11( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric complete continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) Poset) : ( ( ) ( non empty ) set ) ) V12() V18( the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty reflexive transitive antisymmetric complete continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) Poset) : ( ( ) ( non empty ) set ) ) ) CLHomomorphism of S : ( ( ) ( ) 1-sorted ) ,T : ( ( non empty reflexive transitive antisymmetric complete continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) Poset) ) st h9 : ( ( ) ( V7() V10( the carrier of S : ( ( non empty reflexive transitive antisymmetric complete continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) Poset) : ( ( ) ( non empty ) set ) ) V11( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric complete continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) Poset) : ( ( ) ( non empty ) set ) ) V12() V18( the carrier of S : ( ( non empty reflexive transitive antisymmetric complete continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) Poset) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty reflexive transitive antisymmetric complete continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) Poset) : ( ( ) ( non empty ) set ) ) ) CLHomomorphism of S : ( ( non empty reflexive transitive antisymmetric complete continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) Poset) ,b1 : ( ( non empty reflexive transitive antisymmetric complete continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) Poset) ) | A : ( ( ) ( ) NetStr over S : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( V7() V10( the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) V11( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric complete continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) Poset) : ( ( ) ( non empty ) set ) ) ) Element of K32(K33( the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( non empty reflexive transitive antisymmetric complete continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) Poset) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) = f : ( ( V12() V18(A : ( ( ) ( ) Subset of ) , the carrier of b1 : ( ( non empty reflexive transitive antisymmetric complete continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) Poset) : ( ( ) ( non empty ) set ) ) ) ( V7() V10(A : ( ( ) ( ) Subset of ) ) V11( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric complete continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) Poset) : ( ( ) ( non empty ) set ) ) V12() V18(A : ( ( ) ( ) Subset of ) , the carrier of b1 : ( ( non empty reflexive transitive antisymmetric complete continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) Poset) : ( ( ) ( non empty ) set ) ) ) Function of A : ( ( ) ( ) Subset of ) , the carrier of b1 : ( ( non empty reflexive transitive antisymmetric complete continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) Poset) : ( ( ) ( non empty ) set ) ) holds
h9 : ( ( ) ( V7() V10( the carrier of S : ( ( non empty reflexive transitive antisymmetric complete continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) Poset) : ( ( ) ( non empty ) set ) ) V11( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric complete continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) Poset) : ( ( ) ( non empty ) set ) ) V12() V18( the carrier of S : ( ( non empty reflexive transitive antisymmetric complete continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) Poset) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty reflexive transitive antisymmetric complete continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) Poset) : ( ( ) ( non empty ) set ) ) ) CLHomomorphism of S : ( ( non empty reflexive transitive antisymmetric complete continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) Poset) ,b1 : ( ( non empty reflexive transitive antisymmetric complete continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) Poset) ) = h : ( ( ) ( V7() V10( the carrier of S : ( ( non empty reflexive transitive antisymmetric complete continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) Poset) : ( ( ) ( non empty ) set ) ) V11( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric complete continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) Poset) : ( ( ) ( non empty ) set ) ) V12() V18( the carrier of S : ( ( non empty reflexive transitive antisymmetric complete continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) Poset) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty reflexive transitive antisymmetric complete continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) Poset) : ( ( ) ( non empty ) set ) ) ) CLHomomorphism of S : ( ( non empty reflexive transitive antisymmetric complete continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) Poset) ,b1 : ( ( non empty reflexive transitive antisymmetric complete continuous ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous ) Poset) ) ) );
end;

registration
let L be ( ( non empty reflexive transitive antisymmetric upper-bounded ) ( non empty reflexive transitive antisymmetric upper-bounded ) Poset) ;
cluster Filt L : ( ( non empty reflexive transitive antisymmetric upper-bounded ) ( non empty reflexive transitive antisymmetric upper-bounded ) RelStr ) : ( ( ) ( ) set ) -> non empty ;
end;

theorem :: WAYBEL16:9
for X being ( ( ) ( ) set )
for Y being ( ( non empty ) ( non empty ) Subset of ) holds meet Y : ( ( non empty ) ( non empty ) Subset of ) : ( ( ) ( ) set ) is ( ( non empty filtered upper ) ( non empty filtered upper ) Filter of BoolePoset X : ( ( ) ( ) set ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) ) ;

theorem :: WAYBEL16:10
for X being ( ( ) ( ) set )
for Y being ( ( non empty ) ( non empty ) Subset of ) holds
( ex_inf_of Y : ( ( non empty ) ( non empty ) Subset of ) , InclPoset (Filt (BoolePoset X : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) ) : ( ( ) ( non empty ) set ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric ) RelStr ) & "/\" (Y : ( ( non empty ) ( non empty ) Subset of ) ,(InclPoset (Filt (BoolePoset X : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric ) RelStr ) ) : ( ( ) ( ) Element of the carrier of (InclPoset (Filt (BoolePoset b1 : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) ) = meet Y : ( ( non empty ) ( non empty ) Subset of ) : ( ( ) ( ) set ) ) ;

theorem :: WAYBEL16:11
for X being ( ( ) ( ) set ) holds bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of K32(K32(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) is ( ( non empty filtered upper ) ( non empty filtered upper ) Filter of BoolePoset X : ( ( ) ( ) set ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) ) ;

theorem :: WAYBEL16:12
for X being ( ( ) ( ) set ) holds {X : ( ( ) ( ) set ) } : ( ( ) ( non empty finite ) set ) is ( ( non empty filtered upper ) ( non empty filtered upper ) Filter of BoolePoset X : ( ( ) ( ) set ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) ) ;

theorem :: WAYBEL16:13
for X being ( ( ) ( ) set ) holds InclPoset (Filt (BoolePoset X : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) ) : ( ( ) ( non empty ) set ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric ) RelStr ) is upper-bounded ;

theorem :: WAYBEL16:14
for X being ( ( ) ( ) set ) holds InclPoset (Filt (BoolePoset X : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) ) : ( ( ) ( non empty ) set ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric ) RelStr ) is lower-bounded ;

theorem :: WAYBEL16:15
for X being ( ( ) ( ) set ) holds Top (InclPoset (Filt (BoolePoset X : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( ) Element of the carrier of (InclPoset (Filt (BoolePoset b1 : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) ) = bool X : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of K32(K32(b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL16:16
for X being ( ( ) ( ) set ) holds Bottom (InclPoset (Filt (BoolePoset X : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( ) Element of the carrier of (InclPoset (Filt (BoolePoset b1 : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) ) = {X : ( ( ) ( ) set ) } : ( ( ) ( non empty finite ) set ) ;

theorem :: WAYBEL16:17
for X being ( ( non empty ) ( non empty ) set )
for Y being ( ( non empty ) ( non empty ) Subset of ) st ex_sup_of Y : ( ( non empty ) ( non empty ) Subset of ) , InclPoset X : ( ( non empty ) ( non empty ) set ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric ) RelStr ) holds
union Y : ( ( non empty ) ( non empty ) Subset of ) : ( ( ) ( ) set ) c= sup Y : ( ( non empty ) ( non empty ) Subset of ) : ( ( ) ( ) Element of the carrier of (InclPoset b1 : ( ( non empty ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL16:18
for L being ( ( reflexive transitive antisymmetric upper-bounded with_infima ) ( non empty reflexive transitive antisymmetric upper-bounded with_infima ) Semilattice) holds InclPoset (Filt L : ( ( reflexive transitive antisymmetric upper-bounded with_infima ) ( non empty reflexive transitive antisymmetric upper-bounded with_infima ) Semilattice) ) : ( ( ) ( non empty ) set ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric ) RelStr ) is complete ;

registration
let L be ( ( reflexive transitive antisymmetric upper-bounded with_infima ) ( non empty reflexive transitive antisymmetric upper-bounded with_infima ) Semilattice) ;
cluster InclPoset (Filt L : ( ( reflexive transitive antisymmetric upper-bounded with_infima ) ( non empty reflexive transitive antisymmetric upper-bounded with_infima ) RelStr ) ) : ( ( ) ( non empty ) set ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric ) RelStr ) -> strict complete ;
end;

begin

definition
let L be ( ( non empty ) ( non empty ) RelStr ) ;
let p be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
attr p is completely-irreducible means :: WAYBEL16:def 3
 ex_min_of (uparrow p : ( ( V12() V18( the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) : ( ( ) ( non empty ) set ) ) closure ) ( V7() V10( the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) : ( ( ) ( non empty ) set ) ) V11( the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) : ( ( ) ( non empty ) set ) ) V12() V18( the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) : ( ( ) ( non empty ) set ) ) closure ) Element of K32(K33( the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K32( the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) \ {p : ( ( V12() V18( the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) : ( ( ) ( non empty ) set ) ) closure ) ( V7() V10( the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) : ( ( ) ( non empty ) set ) ) V11( the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) : ( ( ) ( non empty ) set ) ) V12() V18( the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) : ( ( ) ( non empty ) set ) ) closure ) Element of K32(K33( the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty finite ) Element of K32( the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K32( the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,L : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) ;
end;

theorem :: WAYBEL16:19
for L being ( ( non empty ) ( non empty ) RelStr )
for p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is completely-irreducible holds
"/\" (((uparrow p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K32( the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) \ {p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty finite ) Element of K32( the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K32( the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,L : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) <> p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

definition
let L be ( ( non empty ) ( non empty ) RelStr ) ;
func Irr L -> ( ( ) ( ) Subset of ) means :: WAYBEL16:def 4
 for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in it : ( ( V12() V18( the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) : ( ( ) ( non empty ) set ) ) closure ) ( V7() V10( the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) : ( ( ) ( non empty ) set ) ) V11( the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) : ( ( ) ( non empty ) set ) ) V12() V18( the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) : ( ( ) ( non empty ) set ) ) closure ) Element of K32(K33( the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) iff x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is completely-irreducible );
end;

theorem :: WAYBEL16:20
for L being ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset)
for p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is completely-irreducible iff ex q being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) < q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & ( for s being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) < s : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= s : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) & uparrow p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty filtered upper ) Element of K32( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = {p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty finite ) Element of K32( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) \/ (uparrow q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty filtered upper ) Element of K32( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of K32( the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: WAYBEL16:21
for L being ( ( non empty reflexive transitive antisymmetric upper-bounded ) ( non empty reflexive transitive antisymmetric upper-bounded ) Poset) holds not Top L : ( ( non empty reflexive transitive antisymmetric upper-bounded ) ( non empty reflexive transitive antisymmetric upper-bounded ) Poset) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty reflexive transitive antisymmetric upper-bounded ) ( non empty reflexive transitive antisymmetric upper-bounded ) Poset) : ( ( ) ( non empty ) set ) ) in Irr L : ( ( non empty reflexive transitive antisymmetric upper-bounded ) ( non empty reflexive transitive antisymmetric upper-bounded ) Poset) : ( ( ) ( ) Subset of ) ;

theorem :: WAYBEL16:22
for L being ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima ) Semilattice) holds Irr L : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima ) Semilattice) : ( ( ) ( ) Subset of ) c= IRR L : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima ) Semilattice) : ( ( ) ( ) Element of K32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima ) Semilattice) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL16:23
for L being ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima ) Semilattice)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is completely-irreducible holds
x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is irreducible ;

theorem :: WAYBEL16:24
for L being ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is completely-irreducible holds
for X being ( ( ) ( ) Subset of ) st ex_inf_of X : ( ( ) ( ) Subset of ) ,L : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = inf X : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( non empty ) set ) ) holds
x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in X : ( ( ) ( ) Subset of ) ;

theorem :: WAYBEL16:25
for L being ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset)
for X being ( ( ) ( ) Subset of ) st X : ( ( ) ( ) Subset of ) is order-generating holds
Irr L : ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) : ( ( ) ( ) Subset of ) c= X : ( ( ) ( ) Subset of ) ;

theorem :: WAYBEL16:26
for L being ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete ) LATTICE)
for p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st ex k being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is_maximal_in the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) \ (uparrow k : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty filtered upper ) Element of K32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) holds
p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is completely-irreducible ;

theorem :: WAYBEL16:27
for L being ( ( transitive antisymmetric with_suprema ) ( non empty transitive antisymmetric with_suprema ) RelStr )
for p, q, u being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) < q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & ( for s being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) < s : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= s : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) & not u : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "\/" u : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( transitive antisymmetric with_suprema ) ( non empty transitive antisymmetric with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) ) = q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "\/" u : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( transitive antisymmetric with_suprema ) ( non empty transitive antisymmetric with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL16:28
for L being ( ( reflexive transitive antisymmetric distributive with_suprema with_infima ) ( non empty reflexive transitive antisymmetric distributive with_suprema with_infima ) LATTICE)
for p, q, u being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) < q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & ( for s being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) < s : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= s : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) & not u : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
not u : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\" q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima ) ( non empty reflexive transitive antisymmetric distributive with_suprema with_infima ) LATTICE) : ( ( ) ( non empty ) set ) ) <= p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL16:29
for L being ( ( reflexive transitive antisymmetric distributive with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete distributive with_suprema with_infima complete ) LATTICE) st L : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete distributive with_suprema with_infima complete ) LATTICE) opp : ( ( strict ) ( non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete distributive with_suprema with_infima complete ) RelStr ) is meet-continuous holds
for p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is completely-irreducible holds
the carrier of L : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete distributive with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) \ (downarrow p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty directed lower ) Element of K32( the carrier of b1 : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete distributive with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K32( the carrier of b1 : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete distributive with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) is ( ( non empty filtered upper Open ) ( non empty filtered upper Open ) Filter of L : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete distributive with_suprema with_infima complete ) LATTICE) ) ;

theorem :: WAYBEL16:30
for L being ( ( reflexive transitive antisymmetric distributive with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete distributive with_suprema with_infima complete ) LATTICE) st L : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete distributive with_suprema with_infima complete ) LATTICE) opp : ( ( strict ) ( non empty strict reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete distributive with_suprema with_infima complete ) RelStr ) is meet-continuous holds
for p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is completely-irreducible holds
ex k being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( k : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in the carrier of (CompactSublatt L : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete distributive with_suprema with_infima complete ) LATTICE) ) : ( ( strict V128(b1 : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete distributive with_suprema with_infima complete ) LATTICE) ) ) ( non empty strict reflexive transitive antisymmetric V128(b1 : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete distributive with_suprema with_infima complete ) LATTICE) ) join-inheriting with_suprema ) SubRelStr of b1 : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete distributive with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( non empty ) set ) & p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is_maximal_in the carrier of L : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete distributive with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) \ (uparrow k : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty filtered upper ) Element of K32( the carrier of b1 : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete distributive with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K32( the carrier of b1 : ( ( reflexive transitive antisymmetric distributive with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete distributive with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: WAYBEL16:31
for L being ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE)
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st not y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
ex p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is completely-irreducible & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & not y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ;

theorem :: WAYBEL16:32
for L being ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) holds
( Irr L : ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( ) Subset of ) is order-generating & ( for X being ( ( ) ( ) Subset of ) st X : ( ( ) ( ) Subset of ) is order-generating holds
Irr L : ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( ) Subset of ) c= X : ( ( ) ( ) Subset of ) ) ) ;

theorem :: WAYBEL16:33
for L being ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE)
for s being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds s : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = "/\" (((uparrow s : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty filtered upper ) Element of K32( the carrier of b1 : ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) /\ (Irr L : ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) ) : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of K32( the carrier of b1 : ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ,L : ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( reflexive transitive antisymmetric lower-bounded with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL16:34
for L being ( ( non empty reflexive transitive antisymmetric complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete ) Poset)
for X being ( ( ) ( ) Subset of )
for p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is completely-irreducible & p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = inf X : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty reflexive transitive antisymmetric complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete ) Poset) : ( ( ) ( non empty ) set ) ) holds
p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in X : ( ( ) ( ) Subset of ) ;

theorem :: WAYBEL16:35
for L being ( ( reflexive transitive antisymmetric with_suprema with_infima complete algebraic ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE)
for p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is completely-irreducible holds
p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = "/\" ( { x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) where x is ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in uparrow p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty filtered upper ) Element of K32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete algebraic ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) & ex k being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( k : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in the carrier of (CompactSublatt L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete algebraic ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) ) : ( ( strict V128(b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete algebraic ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) ) ) ( non empty strict reflexive transitive antisymmetric V128(b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete algebraic ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) ) join-inheriting with_suprema ) SubRelStr of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete algebraic ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) ) : ( ( ) ( non empty ) set ) & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is_maximal_in the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete algebraic ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) \ (uparrow k : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty filtered upper ) Element of K32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete algebraic ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete algebraic ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) } ,L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete algebraic ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete algebraic ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL16:36
for L being ( ( reflexive transitive antisymmetric with_suprema with_infima complete algebraic ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE)
for p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( ex k being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st
( k : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in the carrier of (CompactSublatt L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete algebraic ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) ) : ( ( strict V128(b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete algebraic ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) ) ) ( non empty strict reflexive transitive antisymmetric V128(b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete algebraic ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) ) join-inheriting with_suprema ) SubRelStr of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete algebraic ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) ) : ( ( ) ( non empty ) set ) & p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is_maximal_in the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete algebraic ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) \ (uparrow k : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty filtered upper ) Element of K32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete algebraic ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete algebraic ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V127() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) iff p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is completely-irreducible ) ;