cluster InclPoset (Filt L : ( ( non empty V67() V68() V69() upper-bounded with_infima ) ( non empty V67() V68() V69() upper-bounded with_infima ) RelStr ) ) : ( ( ) ( non empty ) set ) : ( ( strict ) ( non empty strict V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete up-complete /\-complete ) RelStr ) -> strict continuous ;

cluster -> non empty for ( ( ) ( ) Element of the carrier of (InclPoset (Filt L : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( strict ) ( strict V67() V68() V69() ) RelStr ) : ( ( ) ( ) set ) ) ;

pred A is_FreeGen_set_of S means :: WAYBEL22:def 1
for T being ( ( non empty V67() V68() V69() complete continuous ) ( non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete ) Poset)
for f being ( ( Function-like quasi_total ) ( Relation-like A : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( non empty V67() V68() V69() complete continuous ) ( non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like V27(A : ( ( ) ( ) set ) ) quasi_total ) Function of A : ( ( ) ( ) set ) , the carrier of T : ( ( non empty V67() V68() V69() complete continuous ) ( non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete ) Poset) : ( ( ) ( non empty ) set ) ) ex h being ( ( ) ( non empty Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( non empty V67() V68() V69() complete continuous ) ( non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like V27( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) quasi_total ) CLHomomorphism of S : ( ( ) ( ) set ) ,T : ( ( non empty V67() V68() V69() complete continuous ) ( non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete ) Poset) ) st
( h : ( ( ) ( non empty Relation-like the carrier of S : ( ( non empty V67() V68() V69() complete continuous ) ( non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty V67() V68() V69() complete continuous ) ( non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like V27( the carrier of S : ( ( non empty V67() V68() V69() complete continuous ) ( non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete ) Poset) : ( ( ) ( non empty ) set ) ) quasi_total ) CLHomomorphism of S : ( ( non empty V67() V68() V69() complete continuous ) ( non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete ) Poset) ,b₁ : ( ( non empty V67() V68() V69() complete continuous ) ( non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete ) Poset) ) | A : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like A : ( ( ) ( ) set ) -defined the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of S : ( ( non empty V67() V68() V69() complete continuous ) ( non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty V67() V68() V69() complete continuous ) ( non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [: the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of b₁ : ( ( non empty V67() V68() V69() complete continuous ) ( non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete ) Poset) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) = f : ( ( Function-like quasi_total ) ( Relation-like A : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( non empty V67() V68() V69() complete continuous ) ( non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like V27(A : ( ( ) ( ) set ) ) quasi_total ) Function of A : ( ( ) ( ) set ) , the carrier of b₁ : ( ( non empty V67() V68() V69() complete continuous ) ( non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete ) Poset) : ( ( ) ( non empty ) set ) ) & ( for h9 being ( ( ) ( non empty Relation-like the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( non empty V67() V68() V69() complete continuous ) ( non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like V27( the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) quasi_total ) CLHomomorphism of S : ( ( ) ( ) set ) ,T : ( ( non empty V67() V68() V69() complete continuous ) ( non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete ) Poset) ) st h9 : ( ( ) ( non empty Relation-like the carrier of S : ( ( non empty V67() V68() V69() complete continuous ) ( non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty V67() V68() V69() complete continuous ) ( non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like V27( the carrier of S : ( ( non empty V67() V68() V69() complete continuous ) ( non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete ) Poset) : ( ( ) ( non empty ) set ) ) quasi_total ) CLHomomorphism of S : ( ( non empty V67() V68() V69() complete continuous ) ( non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete ) Poset) ,b₁ : ( ( non empty V67() V68() V69() complete continuous ) ( non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete ) Poset) ) | A : ( ( ) ( ) set ) : ( ( Function-like ) ( Relation-like A : ( ( ) ( ) set ) -defined the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of S : ( ( non empty V67() V68() V69() complete continuous ) ( non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty V67() V68() V69() complete continuous ) ( non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like ) Element of bool [: the carrier of S : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of b₁ : ( ( non empty V67() V68() V69() complete continuous ) ( non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete ) Poset) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) = f : ( ( Function-like quasi_total ) ( Relation-like A : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( non empty V67() V68() V69() complete continuous ) ( non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like V27(A : ( ( ) ( ) set ) ) quasi_total ) Function of A : ( ( ) ( ) set ) , the carrier of b₁ : ( ( non empty V67() V68() V69() complete continuous ) ( non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete ) Poset) : ( ( ) ( non empty ) set ) ) holds
h9 : ( ( ) ( non empty Relation-like the carrier of S : ( ( non empty V67() V68() V69() complete continuous ) ( non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty V67() V68() V69() complete continuous ) ( non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like V27( the carrier of S : ( ( non empty V67() V68() V69() complete continuous ) ( non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete ) Poset) : ( ( ) ( non empty ) set ) ) quasi_total ) CLHomomorphism of S : ( ( non empty V67() V68() V69() complete continuous ) ( non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete ) Poset) ,b₁ : ( ( non empty V67() V68() V69() complete continuous ) ( non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete ) Poset) ) = h : ( ( ) ( non empty Relation-like the carrier of S : ( ( non empty V67() V68() V69() complete continuous ) ( non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete ) Poset) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty V67() V68() V69() complete continuous ) ( non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete ) Poset) : ( ( ) ( non empty ) set ) -valued Function-like V27( the carrier of S : ( ( non empty V67() V68() V69() complete continuous ) ( non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete ) Poset) : ( ( ) ( non empty ) set ) ) quasi_total ) CLHomomorphism of S : ( ( non empty V67() V68() V69() complete continuous ) ( non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete ) Poset) ,b₁ : ( ( non empty V67() V68() V69() complete continuous ) ( non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete ) Poset) ) ) );

func FixedUltraFilters X -> ( ( ) ( ) Subset-Family of ) equals :: WAYBEL22:def 2
{ (uparrow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool the carrier of (BoolePoset X : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict V67() V68() V69() lower-bounded upper-bounded V149() V155() V156() with_suprema with_infima complete continuous up-complete /\-complete ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) where x is ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ex z being ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = {z : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) } : ( ( ) ( non empty ) set ) } ;

func f -extension_to_hom -> ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (InclPoset (Filt (BoolePoset X : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict V67() V68() V69() lower-bounded upper-bounded V149() V155() V156() with_suprema with_infima complete continuous up-complete /\-complete ) RelStr ) ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like V27( the carrier of (InclPoset (Filt (BoolePoset X : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict V67() V68() V69() lower-bounded upper-bounded V149() V155() V156() with_suprema with_infima complete continuous up-complete /\-complete ) RelStr ) ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( ) set ) ) means :: WAYBEL22:def 3
for Fi being ( ( ) ( non empty ) Element of ( ( ) ( non empty ) set ) ) holds it : ( ( Function-like quasi_total ) ( Relation-like L : ( ( ) ( ) set ) -defined the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued Function-like quasi_total ) Element of bool [:L : ( ( ) ( ) set ) , the carrier of X : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) . Fi : ( ( ) ( non empty ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) = "\/" ( { ("/\" ( { (f : ( ( ) ( Relation-like L : ( ( ) ( ) set ) -defined L : ( ( ) ( ) set ) -valued ) Element of bool [:L : ( ( ) ( ) set ) ,L : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) . (uparrow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool the carrier of (BoolePoset X : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict V67() V68() V69() lower-bounded upper-bounded V149() V155() V156() with_suprema with_infima complete continuous up-complete /\-complete ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) set ) where x is ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ex z being ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) st
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = {z : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) } : ( ( ) ( non empty ) set ) & z : ( ( ) ( ) Element of X : ( ( ) ( ) set ) ) in Y : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) ) } ,L : ( ( ) ( ) set ) )) : ( ( ) ( ) Element of the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) where Y is ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) : Y : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) in Fi : ( ( ) ( non empty ) Element of ( ( ) ( non empty ) set ) ) } ,L : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ;

cluster f : ( ( Function-like quasi_total ) ( Relation-like FixedUltraFilters X : ( ( ) ( ) set ) : ( ( ) ( ) Subset-Family of ) -defined the carrier of L : ( ( non empty V67() V68() V69() complete continuous ) ( non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V27( FixedUltraFilters X : ( ( ) ( ) set ) : ( ( ) ( ) Subset-Family of ) ) quasi_total ) Element of bool [:(FixedUltraFilters X : ( ( ) ( ) set ) ) : ( ( ) ( ) Subset-Family of ) , the carrier of L : ( ( non empty V67() V68() V69() complete continuous ) ( non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) -extension_to_hom : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (InclPoset (Filt (BoolePoset X : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict V67() V68() V69() lower-bounded upper-bounded V149() V155() V156() with_suprema with_infima complete continuous up-complete /\-complete ) RelStr ) ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of L : ( ( non empty V67() V68() V69() complete continuous ) ( non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V27( the carrier of (InclPoset (Filt (BoolePoset X : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict V67() V68() V69() lower-bounded upper-bounded V149() V155() V156() with_suprema with_infima complete continuous up-complete /\-complete ) RelStr ) ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) -> Function-like quasi_total directed-sups-preserving ;

cluster f : ( ( Function-like quasi_total ) ( Relation-like FixedUltraFilters X : ( ( ) ( ) set ) : ( ( ) ( ) Subset-Family of ) -defined the carrier of L : ( ( non empty V67() V68() V69() complete continuous ) ( non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V27( FixedUltraFilters X : ( ( ) ( ) set ) : ( ( ) ( ) Subset-Family of ) ) quasi_total ) Element of bool [:(FixedUltraFilters X : ( ( ) ( ) set ) ) : ( ( ) ( ) Subset-Family of ) , the carrier of L : ( ( non empty V67() V68() V69() complete continuous ) ( non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) -extension_to_hom : ( ( Function-like quasi_total ) ( non empty Relation-like the carrier of (InclPoset (Filt (BoolePoset X : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict V67() V68() V69() lower-bounded upper-bounded V149() V155() V156() with_suprema with_infima complete continuous up-complete /\-complete ) RelStr ) ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of L : ( ( non empty V67() V68() V69() complete continuous ) ( non empty V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V27( the carrier of (InclPoset (Filt (BoolePoset X : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict V67() V68() V69() lower-bounded upper-bounded V149() V155() V156() with_suprema with_infima complete continuous up-complete /\-complete ) RelStr ) ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict V67() V68() V69() lower-bounded upper-bounded V149() with_suprema with_infima complete continuous up-complete /\-complete ) RelStr ) : ( ( ) ( non empty ) set ) ) quasi_total directed-sups-preserving ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) -> Function-like quasi_total infs-preserving ;