:: WAYBEL_8 semantic presentation

begin

definition
let L be ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ;
func CompactSublatt L -> ( ( strict full ) ( strict reflexive full ) SubRelStr of L : ( ( ) ( ) 1-sorted ) ) means :: WAYBEL_8:def 1
 for x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in the carrier of it : ( ( ) ( ) NetStr over L : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) set ) iff x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is compact );
end;

registration
let L be ( ( non empty reflexive antisymmetric lower-bounded ) ( non empty reflexive antisymmetric lower-bounded ) RelStr ) ;
cluster CompactSublatt L : ( ( non empty reflexive antisymmetric lower-bounded ) ( non empty reflexive antisymmetric lower-bounded ) RelStr ) : ( ( strict full ) ( strict reflexive antisymmetric full ) SubRelStr of L : ( ( non empty reflexive antisymmetric lower-bounded ) ( non empty reflexive antisymmetric lower-bounded ) RelStr ) ) -> non empty strict full ;
end;

theorem :: WAYBEL_8:1
for L being ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete ) LATTICE)
for x, y, k being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= k : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & k : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & k : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in the carrier of (CompactSublatt L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete ) LATTICE) ) : ( ( strict full ) ( non empty strict reflexive transitive antisymmetric full ) SubRelStr of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete ) LATTICE) ) : ( ( ) ( non empty ) set ) holds
x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) << y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL_8:2
for L being ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete ) LATTICE)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( uparrow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty filtered upper ) Element of bool the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-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 with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete ) LATTICE) ) iff x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is compact ) ;

theorem :: WAYBEL_8:3
for L being ( ( non empty reflexive transitive antisymmetric with_suprema lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema lower-bounded ) Poset) holds
( CompactSublatt L : ( ( non empty reflexive transitive antisymmetric with_suprema lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema lower-bounded ) Poset) : ( ( strict full ) ( non empty strict reflexive transitive antisymmetric full ) SubRelStr of b1 : ( ( non empty reflexive transitive antisymmetric with_suprema lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema lower-bounded ) Poset) ) is join-inheriting & Bottom L : ( ( non empty reflexive transitive antisymmetric with_suprema lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema lower-bounded ) Poset) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty reflexive transitive antisymmetric with_suprema lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema lower-bounded ) Poset) : ( ( ) ( non empty ) set ) ) in the carrier of (CompactSublatt L : ( ( non empty reflexive transitive antisymmetric with_suprema lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema lower-bounded ) Poset) ) : ( ( strict full ) ( non empty strict reflexive transitive antisymmetric full ) SubRelStr of b1 : ( ( non empty reflexive transitive antisymmetric with_suprema lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema lower-bounded ) Poset) ) : ( ( ) ( non empty ) set ) ) ;

definition
let L be ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ;
let x be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
func compactbelow x -> ( ( ) ( ) Subset of ) equals :: WAYBEL_8:def 2
 { y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) where y is ( ( ) ( ) Element of ( ( ) ( ) set ) ) : ( x : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete ) RelStr ) >= y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is compact ) } ;
end;

theorem :: WAYBEL_8:4
for L being ( ( non empty reflexive ) ( non empty reflexive ) RelStr )
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in compactbelow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ) iff ( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) >= y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is compact ) ) ;

theorem :: WAYBEL_8:5
for L being ( ( non empty reflexive ) ( non empty reflexive ) RelStr )
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds compactbelow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ) = (downarrow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty directed ) Element of bool the carrier of b1 : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) /\ the carrier of (CompactSublatt L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) : ( ( strict full ) ( strict reflexive full ) SubRelStr of b1 : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL_8:6
for L being ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr )
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds compactbelow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ) c= waybelow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( lower ) Element of bool the carrier of b1 : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

registration
let L be ( ( non empty reflexive antisymmetric lower-bounded ) ( non empty reflexive antisymmetric lower-bounded ) RelStr ) ;
let x be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
cluster compactbelow x : ( ( ) ( ) Element of the carrier of L : ( ( non empty reflexive antisymmetric lower-bounded ) ( non empty reflexive antisymmetric lower-bounded ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ) -> non empty ;
end;

begin

definition
let L be ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ;
attr L is satisfying_axiom_K means :: WAYBEL_8:def 3
 for x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = sup (compactbelow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of the carrier of L : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ;
end;

definition
let L be ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ;
attr L is algebraic means :: WAYBEL_8:def 4
( ( for x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
( not compactbelow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ) is empty & compactbelow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ) is directed ) ) & L : ( ( ) ( ) set ) is up-complete & L : ( ( ) ( ) set ) is satisfying_axiom_K );
end;

theorem :: WAYBEL_8:7
for L being ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric with_suprema with_infima ) LATTICE) holds
( L : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric with_suprema with_infima ) LATTICE) is algebraic iff ( L : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric with_suprema with_infima ) LATTICE) is continuous & ( for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) << y : ( ( ) ( ) 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 ) ( non empty reflexive transitive antisymmetric with_suprema with_infima ) LATTICE) ) : ( ( strict full ) ( strict reflexive transitive antisymmetric full ) SubRelStr of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric with_suprema with_infima ) LATTICE) ) : ( ( ) ( ) set ) & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= k : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & k : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) ) ) ;

registration
cluster reflexive transitive antisymmetric with_suprema with_infima algebraic -> reflexive transitive antisymmetric with_suprema with_infima continuous for ( ( ) ( ) RelStr ) ;
end;

registration
cluster non empty reflexive algebraic -> non empty reflexive up-complete satisfying_axiom_K for ( ( ) ( ) RelStr ) ;
end;

registration
let L be ( ( non empty reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) Poset) ;
cluster CompactSublatt L : ( ( non empty reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) RelStr ) : ( ( strict full ) ( strict reflexive transitive antisymmetric full ) SubRelStr of L : ( ( non empty reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) RelStr ) ) -> strict full join-inheriting ;
end;

definition
let L be ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ;
attr L is arithmetic means :: WAYBEL_8:def 5
( L : ( ( ) ( ) set ) is algebraic & CompactSublatt L : ( ( ) ( ) set ) : ( ( strict full ) ( strict reflexive full ) SubRelStr of L : ( ( ) ( ) set ) ) is meet-inheriting );
end;

begin

registration
cluster reflexive transitive antisymmetric with_suprema with_infima arithmetic -> reflexive transitive antisymmetric with_suprema with_infima algebraic for ( ( ) ( ) RelStr ) ;
end;

registration
cluster trivial reflexive transitive antisymmetric with_suprema with_infima -> reflexive transitive antisymmetric with_suprema with_infima arithmetic for ( ( ) ( ) RelStr ) ;
end;

registration
cluster non empty 1 : ( ( ) ( non empty V35() V36() V37() V41() finite cardinal ) Element of K133() : ( ( ) ( non empty non trivial V35() V36() V37() non finite cardinal limit_cardinal ) Element of bool K129() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) -element strict reflexive transitive antisymmetric with_suprema with_infima for ( ( ) ( ) RelStr ) ;
end;

theorem :: WAYBEL_8:8
for L1, L2 being ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric ) RelStr ) st RelStr(# the carrier of L1 : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) , the InternalRel of L1 : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric ) RelStr ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b1 : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) = RelStr(# the carrier of L2 : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) , the InternalRel of L2 : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric ) RelStr ) : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b2 : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) & L1 : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric ) RelStr ) is up-complete holds
for x1, y1 being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for x2, y2 being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st x1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = x2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & y1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = y2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & x1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) << y1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
x2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) << y2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL_8:9
for L1, L2 being ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric ) RelStr ) st RelStr(# the carrier of L1 : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) , the InternalRel of L1 : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric ) RelStr ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b1 : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) = RelStr(# the carrier of L2 : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) , the InternalRel of L2 : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric ) RelStr ) : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b2 : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) & L1 : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric ) RelStr ) is up-complete holds
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is compact holds
y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is compact ;

theorem :: WAYBEL_8:10
for L1, L2 being ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete ) RelStr ) st RelStr(# the carrier of L1 : ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) , the InternalRel of L1 : ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete ) RelStr ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b1 : ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) = RelStr(# the carrier of L2 : ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) , the InternalRel of L2 : ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete ) RelStr ) : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b2 : ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) holds
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
compactbelow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ) = compactbelow y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ) ;

theorem :: WAYBEL_8:11
for L1, L2 being ( ( ) ( ) RelStr ) st RelStr(# the carrier of L1 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the InternalRel of L1 : ( ( ) ( ) RelStr ) : ( ( ) ( Relation-like the carrier of b1 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -defined the carrier of b1 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -valued ) Element of bool [: the carrier of b1 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) = RelStr(# the carrier of L2 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the InternalRel of L2 : ( ( ) ( ) RelStr ) : ( ( ) ( Relation-like the carrier of b2 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -valued ) Element of bool [: the carrier of b2 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the carrier of b2 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) & not L1 : ( ( ) ( ) RelStr ) is empty holds
not L2 : ( ( ) ( ) RelStr ) is empty ;

theorem :: WAYBEL_8:12
for L1, L2 being ( ( ) ( ) RelStr ) st RelStr(# the carrier of L1 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the InternalRel of L1 : ( ( ) ( ) RelStr ) : ( ( ) ( Relation-like the carrier of b1 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -defined the carrier of b1 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -valued ) Element of bool [: the carrier of b1 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) = RelStr(# the carrier of L2 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the InternalRel of L2 : ( ( ) ( ) RelStr ) : ( ( ) ( Relation-like the carrier of b2 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -valued ) Element of bool [: the carrier of b2 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the carrier of b2 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) & L1 : ( ( ) ( ) RelStr ) is reflexive holds
L2 : ( ( ) ( ) RelStr ) is reflexive ;

theorem :: WAYBEL_8:13
for L1, L2 being ( ( ) ( ) RelStr ) st RelStr(# the carrier of L1 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the InternalRel of L1 : ( ( ) ( ) RelStr ) : ( ( ) ( Relation-like the carrier of b1 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -defined the carrier of b1 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -valued ) Element of bool [: the carrier of b1 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) = RelStr(# the carrier of L2 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the InternalRel of L2 : ( ( ) ( ) RelStr ) : ( ( ) ( Relation-like the carrier of b2 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -valued ) Element of bool [: the carrier of b2 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the carrier of b2 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) & L1 : ( ( ) ( ) RelStr ) is transitive holds
L2 : ( ( ) ( ) RelStr ) is transitive ;

theorem :: WAYBEL_8:14
for L1, L2 being ( ( ) ( ) RelStr ) st RelStr(# the carrier of L1 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the InternalRel of L1 : ( ( ) ( ) RelStr ) : ( ( ) ( Relation-like the carrier of b1 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -defined the carrier of b1 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -valued ) Element of bool [: the carrier of b1 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) = RelStr(# the carrier of L2 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the InternalRel of L2 : ( ( ) ( ) RelStr ) : ( ( ) ( Relation-like the carrier of b2 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -defined the carrier of b2 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) -valued ) Element of bool [: the carrier of b2 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the carrier of b2 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) & L1 : ( ( ) ( ) RelStr ) is antisymmetric holds
L2 : ( ( ) ( ) RelStr ) is antisymmetric ;

theorem :: WAYBEL_8:15
for L1, L2 being ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) st RelStr(# the carrier of L1 : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) , the InternalRel of L1 : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b1 : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) = RelStr(# the carrier of L2 : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) , the InternalRel of L2 : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b2 : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) & L1 : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) is up-complete holds
L2 : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) is up-complete ;

theorem :: WAYBEL_8:16
for L1, L2 being ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete ) RelStr ) st RelStr(# the carrier of L1 : ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) , the InternalRel of L1 : ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete ) RelStr ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b1 : ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) = RelStr(# the carrier of L2 : ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) , the InternalRel of L2 : ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete ) RelStr ) : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b2 : ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) & L1 : ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete ) RelStr ) is satisfying_axiom_K & ( for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( not compactbelow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ) is empty & compactbelow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Subset of ) is directed ) ) holds
L2 : ( ( non empty reflexive antisymmetric up-complete ) ( non empty reflexive antisymmetric up-complete ) RelStr ) is satisfying_axiom_K ;

theorem :: WAYBEL_8:17
for L1, L2 being ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric ) RelStr ) st RelStr(# the carrier of L1 : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) , the InternalRel of L1 : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric ) RelStr ) : ( ( ) ( Relation-like the carrier of b1 : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b1 : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) = RelStr(# the carrier of L2 : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) , the InternalRel of L2 : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric ) RelStr ) : ( ( ) ( Relation-like the carrier of b2 : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b2 : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) & L1 : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric ) RelStr ) is algebraic holds
L2 : ( ( non empty reflexive antisymmetric ) ( non empty reflexive antisymmetric ) RelStr ) is algebraic ;

theorem :: WAYBEL_8:18
for L1, L2 being ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric with_suprema with_infima ) LATTICE) st RelStr(# the carrier of L1 : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric with_suprema with_infima ) LATTICE) : ( ( ) ( non empty ) set ) , the InternalRel of L1 : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric with_suprema with_infima ) LATTICE) : ( ( ) ( Relation-like the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric with_suprema with_infima ) LATTICE) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric with_suprema with_infima ) LATTICE) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric with_suprema with_infima ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric with_suprema with_infima ) LATTICE) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) = RelStr(# the carrier of L2 : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric with_suprema with_infima ) LATTICE) : ( ( ) ( non empty ) set ) , the InternalRel of L2 : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric with_suprema with_infima ) LATTICE) : ( ( ) ( Relation-like the carrier of b2 : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric with_suprema with_infima ) LATTICE) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric with_suprema with_infima ) LATTICE) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b2 : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric with_suprema with_infima ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric with_suprema with_infima ) LATTICE) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) & L1 : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric with_suprema with_infima ) LATTICE) is arithmetic holds
L2 : ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric with_suprema with_infima ) LATTICE) is arithmetic ;

registration
let L be ( ( non empty ) ( non empty ) RelStr ) ;
cluster RelStr(# the carrier of L : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the InternalRel of L : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( Relation-like the carrier of L : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of L : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of L : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) -> non empty strict ;
end;

registration
let L be ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ;
cluster RelStr(# the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) , the InternalRel of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( Relation-like the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict ) RelStr ) -> strict reflexive ;
end;

registration
let L be ( ( transitive ) ( transitive ) RelStr ) ;
cluster RelStr(# the carrier of L : ( ( transitive ) ( transitive ) RelStr ) : ( ( ) ( ) set ) , the InternalRel of L : ( ( transitive ) ( transitive ) RelStr ) : ( ( ) ( Relation-like the carrier of L : ( ( transitive ) ( transitive ) RelStr ) : ( ( ) ( ) set ) -defined the carrier of L : ( ( transitive ) ( transitive ) RelStr ) : ( ( ) ( ) set ) -valued ) Element of bool [: the carrier of L : ( ( transitive ) ( transitive ) RelStr ) : ( ( ) ( ) set ) , the carrier of L : ( ( transitive ) ( transitive ) RelStr ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) -> strict transitive ;
end;

registration
let L be ( ( antisymmetric ) ( antisymmetric ) RelStr ) ;
cluster RelStr(# the carrier of L : ( ( antisymmetric ) ( antisymmetric ) RelStr ) : ( ( ) ( ) set ) , the InternalRel of L : ( ( antisymmetric ) ( antisymmetric ) RelStr ) : ( ( ) ( Relation-like the carrier of L : ( ( antisymmetric ) ( antisymmetric ) RelStr ) : ( ( ) ( ) set ) -defined the carrier of L : ( ( antisymmetric ) ( antisymmetric ) RelStr ) : ( ( ) ( ) set ) -valued ) Element of bool [: the carrier of L : ( ( antisymmetric ) ( antisymmetric ) RelStr ) : ( ( ) ( ) set ) , the carrier of L : ( ( antisymmetric ) ( antisymmetric ) RelStr ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) -> strict antisymmetric ;
end;

registration
let L be ( ( with_infima ) ( non empty with_infima ) RelStr ) ;
cluster RelStr(# the carrier of L : ( ( with_infima ) ( non empty with_infima ) RelStr ) : ( ( ) ( non empty ) set ) , the InternalRel of L : ( ( with_infima ) ( non empty with_infima ) RelStr ) : ( ( ) ( Relation-like the carrier of L : ( ( with_infima ) ( non empty with_infima ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of L : ( ( with_infima ) ( non empty with_infima ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of L : ( ( with_infima ) ( non empty with_infima ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( with_infima ) ( non empty with_infima ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict ) RelStr ) -> strict with_infima ;
end;

registration
let L be ( ( with_suprema ) ( non empty with_suprema ) RelStr ) ;
cluster RelStr(# the carrier of L : ( ( with_suprema ) ( non empty with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) , the InternalRel of L : ( ( with_suprema ) ( non empty with_suprema ) RelStr ) : ( ( ) ( Relation-like the carrier of L : ( ( with_suprema ) ( non empty with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of L : ( ( with_suprema ) ( non empty with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of L : ( ( with_suprema ) ( non empty with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( with_suprema ) ( non empty with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict ) RelStr ) -> strict with_suprema ;
end;

registration
let L be ( ( non empty reflexive up-complete ) ( non empty reflexive up-complete ) RelStr ) ;
cluster RelStr(# the carrier of L : ( ( non empty reflexive up-complete ) ( non empty reflexive up-complete ) RelStr ) : ( ( ) ( non empty ) set ) , the InternalRel of L : ( ( non empty reflexive up-complete ) ( non empty reflexive up-complete ) RelStr ) : ( ( ) ( Relation-like the carrier of L : ( ( non empty reflexive up-complete ) ( non empty reflexive up-complete ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of L : ( ( non empty reflexive up-complete ) ( non empty reflexive up-complete ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of L : ( ( non empty reflexive up-complete ) ( non empty reflexive up-complete ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( non empty reflexive up-complete ) ( non empty reflexive up-complete ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict reflexive ) RelStr ) -> strict up-complete ;
end;

registration
let L be ( ( non empty reflexive antisymmetric algebraic ) ( non empty reflexive antisymmetric up-complete satisfying_axiom_K algebraic ) RelStr ) ;
cluster RelStr(# the carrier of L : ( ( non empty reflexive antisymmetric algebraic ) ( non empty reflexive antisymmetric up-complete satisfying_axiom_K algebraic ) RelStr ) : ( ( ) ( non empty ) set ) , the InternalRel of L : ( ( non empty reflexive antisymmetric algebraic ) ( non empty reflexive antisymmetric up-complete satisfying_axiom_K algebraic ) RelStr ) : ( ( ) ( Relation-like the carrier of L : ( ( non empty reflexive antisymmetric algebraic ) ( non empty reflexive antisymmetric up-complete satisfying_axiom_K algebraic ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of L : ( ( non empty reflexive antisymmetric algebraic ) ( non empty reflexive antisymmetric up-complete satisfying_axiom_K algebraic ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of L : ( ( non empty reflexive antisymmetric algebraic ) ( non empty reflexive antisymmetric up-complete satisfying_axiom_K algebraic ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( non empty reflexive antisymmetric algebraic ) ( non empty reflexive antisymmetric up-complete satisfying_axiom_K algebraic ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict reflexive antisymmetric up-complete ) RelStr ) -> strict algebraic ;
end;

registration
let L be ( ( reflexive transitive antisymmetric with_suprema with_infima arithmetic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) LATTICE) ;
cluster RelStr(# the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima arithmetic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) : ( ( ) ( non empty ) set ) , the InternalRel of L : ( ( reflexive transitive antisymmetric with_suprema with_infima arithmetic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) : ( ( ) ( Relation-like the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima arithmetic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima arithmetic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima arithmetic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima arithmetic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) -> strict arithmetic ;
end;

theorem :: WAYBEL_8:19
for L being ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) holds
( L : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) is arithmetic iff CompactSublatt L : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( strict full ) ( strict reflexive transitive antisymmetric full join-inheriting ) SubRelStr of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) ) is ( ( reflexive transitive antisymmetric with_suprema with_infima ) ( non empty reflexive transitive antisymmetric with_suprema with_infima ) LATTICE) ) ;

theorem :: WAYBEL_8:20
for L being ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) holds
( L : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) is arithmetic iff L : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) -waybelow : ( ( ) ( Relation-like the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) -valued transitive auxiliary(i) auxiliary(ii) auxiliary(iii) auxiliary(iv) auxiliary approximating satisfying_SI satisfying_INT ) Element of bool [: the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is multiplicative ) ;

theorem :: WAYBEL_8:21
for L being ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded arithmetic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic arithmetic ) LATTICE)
for p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is pseudoprime holds
p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is prime ;

theorem :: WAYBEL_8:22
for L being ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded distributive algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) st ( for p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is pseudoprime holds
p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is prime ) holds
L : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded distributive algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) is arithmetic ;

registration
let L be ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) ;
let c be ( ( Function-like V32( the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) closure ) ( Relation-like the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) -defined the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) -valued Function-like V32( the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) projection closure ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ;
cluster non empty directed for ( ( ) ( ) Element of bool the carrier of (Image c : ( ( Function-like V32( the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete 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 with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) : ( ( ) ( non empty ) set ) ) closure ) ( Relation-like the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V32( the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete 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 with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) : ( ( ) ( non empty ) set ) ) projection closure ) Element of bool [: the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete 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 with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict full ) ( non empty strict reflexive transitive antisymmetric full ) SubRelStr of L : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) RelStr ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: WAYBEL_8:23
for L being ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE)
for c being ( ( Function-like V32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) closure ) ( Relation-like the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) -valued Function-like V32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) projection closure ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st c : ( ( Function-like V32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) closure ) ( Relation-like the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) -valued Function-like V32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) projection closure ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is directed-sups-preserving holds
c : ( ( Function-like V32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) closure ) ( Relation-like the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) -valued Function-like V32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) projection closure ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) .: ([#] (CompactSublatt L : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) ) : ( ( strict full ) ( strict reflexive transitive antisymmetric full join-inheriting ) SubRelStr of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) ) ) : ( ( ) ( non proper ) Element of bool the carrier of (CompactSublatt b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) ) : ( ( strict full ) ( strict reflexive transitive antisymmetric full join-inheriting ) SubRelStr of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) c= [#] (CompactSublatt (Image c : ( ( Function-like V32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) closure ) ( Relation-like the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) -valued Function-like V32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) projection closure ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( strict full ) ( non empty strict reflexive transitive antisymmetric full ) SubRelStr of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) ) ) : ( ( strict full ) ( strict reflexive transitive antisymmetric full ) SubRelStr of Image b2 : ( ( Function-like V32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) closure ) ( Relation-like the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) -valued Function-like V32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) projection closure ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( strict full ) ( non empty strict reflexive transitive antisymmetric full ) SubRelStr of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) ) ) : ( ( ) ( non proper ) Element of bool the carrier of (CompactSublatt (Image b2 : ( ( Function-like V32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) closure ) ( Relation-like the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) -valued Function-like V32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) projection closure ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( strict full ) ( non empty strict reflexive transitive antisymmetric full ) SubRelStr of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) ) ) : ( ( strict full ) ( strict reflexive transitive antisymmetric full ) SubRelStr of Image b2 : ( ( Function-like V32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) closure ) ( Relation-like the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) -valued Function-like V32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) projection closure ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( strict full ) ( non empty strict reflexive transitive antisymmetric full ) SubRelStr of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL_8:24
for L being ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE)
for c being ( ( Function-like V32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) closure ) ( Relation-like the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) -valued Function-like V32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) projection closure ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st c : ( ( Function-like V32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) closure ) ( Relation-like the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) -valued Function-like V32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) projection closure ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is directed-sups-preserving holds
Image c : ( ( Function-like V32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) closure ) ( Relation-like the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) -valued Function-like V32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) projection closure ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( strict full ) ( non empty strict reflexive transitive antisymmetric full ) SubRelStr of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) ) is ( ( reflexive transitive antisymmetric with_suprema with_infima algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima upper-bounded up-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) ;

theorem :: WAYBEL_8:25
for L being ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE)
for c being ( ( Function-like V32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) closure ) ( Relation-like the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) -valued Function-like V32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) projection closure ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st c : ( ( Function-like V32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) closure ) ( Relation-like the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) -valued Function-like V32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) projection closure ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is directed-sups-preserving holds
c : ( ( Function-like V32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) closure ) ( Relation-like the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) -valued Function-like V32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) projection closure ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) .: ([#] (CompactSublatt L : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) ) : ( ( strict full ) ( non empty strict reflexive transitive antisymmetric with_suprema full join-inheriting ) SubRelStr of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) ) ) : ( ( ) ( non proper ) Element of bool the carrier of (CompactSublatt b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) ) : ( ( strict full ) ( non empty strict reflexive transitive antisymmetric with_suprema full join-inheriting ) SubRelStr of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = [#] (CompactSublatt (Image c : ( ( Function-like V32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) closure ) ( Relation-like the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) -valued Function-like V32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) projection closure ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( strict full ) ( non empty strict reflexive transitive antisymmetric full ) SubRelStr of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) ) ) : ( ( strict full ) ( strict reflexive transitive antisymmetric full ) SubRelStr of Image b2 : ( ( Function-like V32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) closure ) ( Relation-like the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) -valued Function-like V32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) projection closure ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( strict full ) ( non empty strict reflexive transitive antisymmetric full ) SubRelStr of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) ) ) : ( ( ) ( non proper ) Element of bool the carrier of (CompactSublatt (Image b2 : ( ( Function-like V32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) closure ) ( Relation-like the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) -valued Function-like V32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) projection closure ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( strict full ) ( non empty strict reflexive transitive antisymmetric full ) SubRelStr of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) ) ) : ( ( strict full ) ( strict reflexive transitive antisymmetric full ) SubRelStr of Image b2 : ( ( Function-like V32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) closure ) ( Relation-like the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) -valued Function-like V32( the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) : ( ( ) ( non empty ) set ) ) projection closure ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( strict full ) ( non empty strict reflexive transitive antisymmetric full ) SubRelStr of b1 : ( ( reflexive transitive antisymmetric with_suprema with_infima lower-bounded algebraic ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete satisfying_axiom_of_approximation continuous satisfying_axiom_K algebraic ) LATTICE) ) ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

begin

theorem :: WAYBEL_8:26
for X, x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) is ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) iff x : ( ( ) ( ) set ) c= X : ( ( ) ( ) set ) ) ;

theorem :: WAYBEL_8:27
for X being ( ( ) ( ) set )
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) << y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) iff for Y being ( ( ) ( ) Subset-Family of ) st y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) c= union Y : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) holds
ex Z being ( ( finite ) ( finite ) Subset of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) c= union Z : ( ( finite ) ( finite ) Subset of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: WAYBEL_8:28
for X being ( ( ) ( ) set )
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is finite iff x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is compact ) ;

theorem :: WAYBEL_8:29
for X being ( ( ) ( ) set )
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds compactbelow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Subset of ) = { y : ( ( finite ) ( finite ) Subset of ( ( ) ( non empty ) set ) ) where y is ( ( finite ) ( finite ) Subset of ( ( ) ( non empty ) set ) ) : verum } ;

theorem :: WAYBEL_8:30
for X being ( ( ) ( ) set )
for F being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) holds
( F : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) in the carrier of (CompactSublatt (BoolePoset X : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean ) RelStr ) ) : ( ( strict full ) ( non empty strict reflexive transitive antisymmetric with_suprema full join-inheriting ) SubRelStr of BoolePoset b1 : ( ( ) ( ) set ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean ) RelStr ) ) : ( ( ) ( non empty ) set ) iff F : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) is finite ) ;

registration
let X be ( ( ) ( ) set ) ;
let x be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
cluster compactbelow x : ( ( ) ( ) Element of the carrier of (BoolePoset X : ( ( ) ( ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V226() up-complete /\-complete distributive V266() complemented Boolean ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Subset of ) -> directed lower ;
end;

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

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