WAYBEL33

:: WAYBEL33 semantic presentation

begin

definition

let L be ( ( non empty reflexive transitive antisymmetric ) ( non empty reflexive transitive antisymmetric ) Poset) ;
let X be ( ( non empty ) ( non empty ) Subset of ) ;
let F be ( ( non empty filtered upper ) ( non empty filtered upper ) Filter of BoolePoset X : ( ( non empty ) ( non empty ) Subset of ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete ) RelStr ) ) ;

func lim_inf F -> ( ( ) ( ) Element of ( ( ) ( ) set ) ) equals :: WAYBEL33:def 1
"\/" ( { (inf B : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of the carrier of L : ( ( ) ( ) TopRelStr ) : ( ( ) ( ) set ) ) where B is ( ( ) ( ) Subset of ) : B : ( ( ) ( ) Subset of ) in F : ( ( ) ( ) Element of bool (bool L : ( ( ) ( ) TopRelStr ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) } ,L : ( ( ) ( ) TopRelStr ) ) : ( ( ) ( ) Element of the carrier of L : ( ( ) ( ) TopRelStr ) : ( ( ) ( ) set ) ) ;

end;

theorem :: WAYBEL33:1

for L1, L2 being ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) st RelStr(# the carrier of L1 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) , the InternalRel of L1 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( Relation-like the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) = RelStr(# the carrier of L2 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) , the InternalRel of L2 : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( Relation-like the carrier of b₂ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₂ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) holds
for X1 being ( ( non empty ) ( non empty ) Subset of )
for X2 being ( ( non empty ) ( non empty ) Subset of )
for F1 being ( ( non empty filtered upper ) ( non empty filtered upper ) Filter of BoolePoset X1 : ( ( non empty ) ( non empty ) Subset of ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete ) RelStr ) )
for F2 being ( ( non empty filtered upper ) ( non empty filtered upper ) Filter of BoolePoset X2 : ( ( non empty ) ( non empty ) Subset of ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete ) RelStr ) ) st F1 : ( ( non empty filtered upper ) ( non empty filtered upper ) Filter of BoolePoset b₃ : ( ( non empty ) ( non empty ) Subset of ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete ) RelStr ) ) = F2 : ( ( non empty filtered upper ) ( non empty filtered upper ) Filter of BoolePoset b₄ : ( ( non empty ) ( non empty ) Subset of ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete ) RelStr ) ) holds
lim_inf F1 : ( ( non empty filtered upper ) ( non empty filtered upper ) Filter of BoolePoset b₃ : ( ( non empty ) ( non empty ) Subset of ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete ) RelStr ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = lim_inf F2 : ( ( non empty filtered upper ) ( non empty filtered upper ) Filter of BoolePoset b₄ : ( ( non empty ) ( non empty ) Subset of ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete ) RelStr ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

definition

let L be ( ( non empty ) ( non empty ) TopRelStr ) ;

attr L is lim-inf means :: WAYBEL33:def 2
the topology of L : ( ( ) ( ) TopRelStr ) : ( ( ) ( ) Element of bool (bool the carrier of L : ( ( ) ( ) TopRelStr ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = xi L : ( ( ) ( ) TopRelStr ) : ( ( ) ( ) Element of bool (bool the carrier of L : ( ( ) ( ) TopRelStr ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

end;

registration

cluster non empty lim-inf -> non empty TopSpace-like for ( ( ) ( ) TopRelStr ) ;

end;

registration

cluster trivial TopSpace-like reflexive transitive antisymmetric with_suprema with_infima -> TopSpace-like reflexive transitive antisymmetric with_suprema with_infima lim-inf for ( ( ) ( ) TopRelStr ) ;

end;

registration

cluster non empty TopSpace-like reflexive transitive antisymmetric continuous with_suprema with_infima complete lim-inf for ( ( ) ( ) TopRelStr ) ;

end;

theorem :: WAYBEL33:2

for L1, L2 being ( ( non empty ) ( non empty ) 1-sorted ) st the carrier of L1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) = the carrier of L2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) holds
for N1 being ( ( ) ( ) NetStr over L1 : ( ( non empty ) ( non empty ) 1-sorted ) ) ex N2 being ( ( strict ) ( strict ) NetStr over L2 : ( ( non empty ) ( non empty ) 1-sorted ) ) st
( RelStr(# the carrier of N1 : ( ( ) ( ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( ) set ) , the InternalRel of N1 : ( ( ) ( ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( Relation-like the carrier of b₃ : ( ( ) ( ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( ) set ) -defined the carrier of b₃ : ( ( ) ( ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( ) set ) -valued ) Element of bool [: the carrier of b₃ : ( ( ) ( ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( ) set ) , the carrier of b₃ : ( ( ) ( ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) = RelStr(# the carrier of N2 : ( ( strict ) ( strict ) NetStr over b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( ) set ) , the InternalRel of N2 : ( ( strict ) ( strict ) NetStr over b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( Relation-like the carrier of b₄ : ( ( strict ) ( strict ) NetStr over b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( ) set ) -defined the carrier of b₄ : ( ( strict ) ( strict ) NetStr over b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( ) set ) -valued ) Element of bool [: the carrier of b₄ : ( ( strict ) ( strict ) NetStr over b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( ) set ) , the carrier of b₄ : ( ( strict ) ( strict ) NetStr over b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) & the mapping of N1 : ( ( ) ( ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( Function-like V41( the carrier of b₃ : ( ( ) ( ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b₃ : ( ( ) ( ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V41( the carrier of b₃ : ( ( ) ( ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) Element of bool [: the carrier of b₃ : ( ( ) ( ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) = the mapping of N2 : ( ( strict ) ( strict ) NetStr over b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( Function-like V41( the carrier of b₄ : ( ( strict ) ( strict ) NetStr over b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b₄ : ( ( strict ) ( strict ) NetStr over b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( ) set ) -defined the carrier of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V41( the carrier of b₄ : ( ( strict ) ( strict ) NetStr over b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) Element of bool [: the carrier of b₄ : ( ( strict ) ( strict ) NetStr over b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: WAYBEL33:3

for L1, L2 being ( ( non empty ) ( non empty ) 1-sorted ) st the carrier of L1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) = the carrier of L2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) holds
for N1 being ( ( ) ( ) NetStr over L1 : ( ( non empty ) ( non empty ) 1-sorted ) ) st N1 : ( ( ) ( ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) in NetUniv L1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) holds
ex N2 being ( ( non empty transitive strict directed ) ( non empty transitive strict directed ) net of L2 : ( ( non empty ) ( non empty ) 1-sorted ) ) st
( N2 : ( ( non empty transitive strict directed ) ( non empty transitive strict directed ) net of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) in NetUniv L2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) & RelStr(# the carrier of N1 : ( ( ) ( ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( ) set ) , the InternalRel of N1 : ( ( ) ( ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( Relation-like the carrier of b₃ : ( ( ) ( ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( ) set ) -defined the carrier of b₃ : ( ( ) ( ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( ) set ) -valued ) Element of bool [: the carrier of b₃ : ( ( ) ( ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( ) set ) , the carrier of b₃ : ( ( ) ( ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) = RelStr(# the carrier of N2 : ( ( non empty transitive strict directed ) ( non empty transitive strict directed ) net of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the InternalRel of N2 : ( ( non empty transitive strict directed ) ( non empty transitive strict directed ) net of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( Relation-like the carrier of b₄ : ( ( non empty transitive strict directed ) ( non empty transitive strict directed ) net of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) -defined the carrier of b₄ : ( ( non empty transitive strict directed ) ( non empty transitive strict directed ) net of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₄ : ( ( non empty transitive strict directed ) ( non empty transitive strict directed ) net of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of b₄ : ( ( non empty transitive strict directed ) ( non empty transitive strict directed ) net of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) & the mapping of N1 : ( ( ) ( ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( Function-like V41( the carrier of b₃ : ( ( ) ( ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b₃ : ( ( ) ( ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V41( the carrier of b₃ : ( ( ) ( ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) Element of bool [: the carrier of b₃ : ( ( ) ( ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) = the mapping of N2 : ( ( non empty transitive strict directed ) ( non empty transitive strict directed ) net of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( Function-like V41( the carrier of b₄ : ( ( non empty transitive strict directed ) ( non empty transitive strict directed ) net of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₄ : ( ( non empty transitive strict directed ) ( non empty transitive strict directed ) net of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V41( the carrier of b₄ : ( ( non empty transitive strict directed ) ( non empty transitive strict directed ) net of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) Element of bool [: the carrier of b₄ : ( ( non empty transitive strict directed ) ( non empty transitive strict directed ) net of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: WAYBEL33:4

for L1, L2 being ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) st RelStr(# the carrier of L1 : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) , the InternalRel of L1 : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( Relation-like the carrier of b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) = RelStr(# the carrier of L2 : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) , the InternalRel of L2 : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( Relation-like the carrier of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) holds
for N1 being ( ( non empty transitive directed ) ( non empty transitive directed ) net of L1 : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) )
for N2 being ( ( non empty transitive directed ) ( non empty transitive directed ) net of L2 : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) st RelStr(# the carrier of N1 : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( ) ( non empty ) set ) , the InternalRel of N1 : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( ) ( Relation-like the carrier of b₃ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( ) ( non empty ) set ) -defined the carrier of b₃ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₃ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( ) ( non empty ) set ) , the carrier of b₃ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) = RelStr(# the carrier of N2 : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( ) ( non empty ) set ) , the InternalRel of N2 : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( ) ( Relation-like the carrier of b₄ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( ) ( non empty ) set ) -defined the carrier of b₄ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₄ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( ) ( non empty ) set ) , the carrier of b₄ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) & the mapping of N1 : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( Function-like V41( the carrier of b₃ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₃ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) -valued Function-like V41( the carrier of b₃ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) ) ) Element of bool [: the carrier of b₃ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) = the mapping of N2 : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( Function-like V41( the carrier of b₄ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₄ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) -valued Function-like V41( the carrier of b₄ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) ) ) Element of bool [: the carrier of b₄ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) holds
lim_inf N1 : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) ) = lim_inf N2 : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( ) ( ) Element of the carrier of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL33:5

for L1, L2 being ( ( non empty ) ( non empty ) 1-sorted ) st the carrier of L1 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) = the carrier of L2 : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) holds
for N1 being ( ( non empty transitive directed ) ( non empty transitive directed ) net of L1 : ( ( non empty ) ( non empty ) 1-sorted ) )
for N2 being ( ( non empty transitive directed ) ( non empty transitive directed ) net of L2 : ( ( non empty ) ( non empty ) 1-sorted ) ) st RelStr(# the carrier of N1 : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the InternalRel of N1 : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( Relation-like the carrier of b₃ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) -defined the carrier of b₃ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₃ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of b₃ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) = RelStr(# the carrier of N2 : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the InternalRel of N2 : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( Relation-like the carrier of b₄ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) -defined the carrier of b₄ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₄ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of b₄ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) & the mapping of N1 : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( Function-like V41( the carrier of b₃ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₃ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V41( the carrier of b₃ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) Element of bool [: the carrier of b₃ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) = the mapping of N2 : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( Function-like V41( the carrier of b₄ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₄ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V41( the carrier of b₄ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) Element of bool [: the carrier of b₄ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) holds
for S1 being ( ( ) ( non empty transitive directed ) subnet of N1 : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) ) ex S2 being ( ( strict ) ( non empty transitive strict directed ) subnet of N2 : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) ) st
( RelStr(# the carrier of S1 : ( ( ) ( non empty transitive directed ) subnet of b₃ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) ) : ( ( ) ( non empty ) set ) , the InternalRel of S1 : ( ( ) ( non empty transitive directed ) subnet of b₃ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) ) : ( ( ) ( Relation-like the carrier of b₅ : ( ( ) ( non empty transitive directed ) subnet of b₃ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) ) : ( ( ) ( non empty ) set ) -defined the carrier of b₅ : ( ( ) ( non empty transitive directed ) subnet of b₃ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₅ : ( ( ) ( non empty transitive directed ) subnet of b₃ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) ) : ( ( ) ( non empty ) set ) , the carrier of b₅ : ( ( ) ( non empty transitive directed ) subnet of b₃ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) = RelStr(# the carrier of S2 : ( ( strict ) ( non empty transitive strict directed ) subnet of b₄ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) ) : ( ( ) ( non empty ) set ) , the InternalRel of S2 : ( ( strict ) ( non empty transitive strict directed ) subnet of b₄ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) ) : ( ( ) ( Relation-like the carrier of b₆ : ( ( strict ) ( non empty transitive strict directed ) subnet of b₄ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) ) : ( ( ) ( non empty ) set ) -defined the carrier of b₆ : ( ( strict ) ( non empty transitive strict directed ) subnet of b₄ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₆ : ( ( strict ) ( non empty transitive strict directed ) subnet of b₄ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) ) : ( ( ) ( non empty ) set ) , the carrier of b₆ : ( ( strict ) ( non empty transitive strict directed ) subnet of b₄ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) & the mapping of S1 : ( ( ) ( non empty transitive directed ) subnet of b₃ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) ) : ( ( Function-like V41( the carrier of b₅ : ( ( ) ( non empty transitive directed ) subnet of b₃ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₅ : ( ( ) ( non empty transitive directed ) subnet of b₃ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V41( the carrier of b₅ : ( ( ) ( non empty transitive directed ) subnet of b₃ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) Element of bool [: the carrier of b₅ : ( ( ) ( non empty transitive directed ) subnet of b₃ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) = the mapping of S2 : ( ( strict ) ( non empty transitive strict directed ) subnet of b₄ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) ) : ( ( Function-like V41( the carrier of b₆ : ( ( strict ) ( non empty transitive strict directed ) subnet of b₄ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₆ : ( ( strict ) ( non empty transitive strict directed ) subnet of b₄ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V41( the carrier of b₆ : ( ( strict ) ( non empty transitive strict directed ) subnet of b₄ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) Element of bool [: the carrier of b₆ : ( ( strict ) ( non empty transitive strict directed ) subnet of b₄ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: WAYBEL33:6

for L1, L2 being ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) st RelStr(# the carrier of L1 : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) , the InternalRel of L1 : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( Relation-like the carrier of b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) = RelStr(# the carrier of L2 : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) , the InternalRel of L2 : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( Relation-like the carrier of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) holds
for N1 being ( ( ) ( ) NetStr over L1 : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) )
for a being ( ( ) ( ) set ) st [N1 : ( ( ) ( ) NetStr over b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) ,a : ( ( ) ( ) set ) ] : ( ( ) ( V38() ) set ) in lim_inf-Convergence L1 : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( Relation-like ) Convergence-Class of b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) holds
ex N2 being ( ( non empty transitive strict directed ) ( non empty transitive strict directed ) net of L2 : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) st
( [N2 : ( ( non empty transitive strict directed ) ( non empty transitive strict directed ) net of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) ,a : ( ( ) ( ) set ) ] : ( ( ) ( V38() ) set ) in lim_inf-Convergence L2 : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( Relation-like ) Convergence-Class of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) & RelStr(# the carrier of N1 : ( ( ) ( ) NetStr over b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( ) ( ) set ) , the InternalRel of N1 : ( ( ) ( ) NetStr over b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( ) ( Relation-like the carrier of b₃ : ( ( ) ( ) NetStr over b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( ) ( ) set ) -defined the carrier of b₃ : ( ( ) ( ) NetStr over b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( ) ( ) set ) -valued ) Element of bool [: the carrier of b₃ : ( ( ) ( ) NetStr over b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( ) ( ) set ) , the carrier of b₃ : ( ( ) ( ) NetStr over b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) = RelStr(# the carrier of N2 : ( ( non empty transitive strict directed ) ( non empty transitive strict directed ) net of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( ) ( non empty ) set ) , the InternalRel of N2 : ( ( non empty transitive strict directed ) ( non empty transitive strict directed ) net of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( ) ( Relation-like the carrier of b₅ : ( ( non empty transitive strict directed ) ( non empty transitive strict directed ) net of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( ) ( non empty ) set ) -defined the carrier of b₅ : ( ( non empty transitive strict directed ) ( non empty transitive strict directed ) net of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₅ : ( ( non empty transitive strict directed ) ( non empty transitive strict directed ) net of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( ) ( non empty ) set ) , the carrier of b₅ : ( ( non empty transitive strict directed ) ( non empty transitive strict directed ) net of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) & the mapping of N1 : ( ( ) ( ) NetStr over b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( Function-like V41( the carrier of b₃ : ( ( ) ( ) NetStr over b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( ) ( ) set ) , the carrier of b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b₃ : ( ( ) ( ) NetStr over b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) -valued Function-like V41( the carrier of b₃ : ( ( ) ( ) NetStr over b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( ) ( ) set ) , the carrier of b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) ) ) Element of bool [: the carrier of b₃ : ( ( ) ( ) NetStr over b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( ) ( ) set ) , the carrier of b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) = the mapping of N2 : ( ( non empty transitive strict directed ) ( non empty transitive strict directed ) net of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( Function-like V41( the carrier of b₅ : ( ( non empty transitive strict directed ) ( non empty transitive strict directed ) net of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₅ : ( ( non empty transitive strict directed ) ( non empty transitive strict directed ) net of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) -valued Function-like V41( the carrier of b₅ : ( ( non empty transitive strict directed ) ( non empty transitive strict directed ) net of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) ) ) Element of bool [: the carrier of b₅ : ( ( non empty transitive strict directed ) ( non empty transitive strict directed ) net of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: WAYBEL33:7

for L1, L2 being ( ( non empty ) ( non empty ) 1-sorted )
for N1 being ( ( non empty ) ( non empty ) NetStr over L1 : ( ( non empty ) ( non empty ) 1-sorted ) )
for N2 being ( ( non empty ) ( non empty ) NetStr over L2 : ( ( non empty ) ( non empty ) 1-sorted ) ) st RelStr(# the carrier of N1 : ( ( non empty ) ( non empty ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the InternalRel of N1 : ( ( non empty ) ( non empty ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( Relation-like the carrier of b₃ : ( ( non empty ) ( non empty ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) -defined the carrier of b₃ : ( ( non empty ) ( non empty ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₃ : ( ( non empty ) ( non empty ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of b₃ : ( ( non empty ) ( non empty ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) = RelStr(# the carrier of N2 : ( ( non empty ) ( non empty ) NetStr over b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the InternalRel of N2 : ( ( non empty ) ( non empty ) NetStr over b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( Relation-like the carrier of b₄ : ( ( non empty ) ( non empty ) NetStr over b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) -defined the carrier of b₄ : ( ( non empty ) ( non empty ) NetStr over b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₄ : ( ( non empty ) ( non empty ) NetStr over b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of b₄ : ( ( non empty ) ( non empty ) NetStr over b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) & the mapping of N1 : ( ( non empty ) ( non empty ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( Function-like V41( the carrier of b₃ : ( ( non empty ) ( non empty ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₃ : ( ( non empty ) ( non empty ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V41( the carrier of b₃ : ( ( non empty ) ( non empty ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) Element of bool [: the carrier of b₃ : ( ( non empty ) ( non empty ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) = the mapping of N2 : ( ( non empty ) ( non empty ) NetStr over b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( Function-like V41( the carrier of b₄ : ( ( non empty ) ( non empty ) NetStr over b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₄ : ( ( non empty ) ( non empty ) NetStr over b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V41( the carrier of b₄ : ( ( non empty ) ( non empty ) NetStr over b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) Element of bool [: the carrier of b₄ : ( ( non empty ) ( non empty ) NetStr over b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( non empty ) set ) ) holds
for X being ( ( ) ( ) set ) st N1 : ( ( non empty ) ( non empty ) NetStr over b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) is_eventually_in X : ( ( ) ( ) set ) holds
N2 : ( ( non empty ) ( non empty ) NetStr over b₂ : ( ( non empty ) ( non empty ) 1-sorted ) ) is_eventually_in X : ( ( ) ( ) set ) ;

theorem :: WAYBEL33:8

for L1, L2 being ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) st RelStr(# the carrier of L1 : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) , the InternalRel of L1 : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( Relation-like the carrier of b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) = RelStr(# the carrier of L2 : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) , the InternalRel of L2 : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( Relation-like the carrier of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) holds
ConvergenceSpace (lim_inf-Convergence L1 : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( ) ( Relation-like ) Convergence-Class of b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( strict ) ( non empty strict TopSpace-like ) TopStruct ) = ConvergenceSpace (lim_inf-Convergence L2 : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( ) ( Relation-like ) Convergence-Class of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( strict ) ( non empty strict TopSpace-like ) TopStruct ) ;

theorem :: WAYBEL33:9

for L1, L2 being ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) st RelStr(# the carrier of L1 : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) , the InternalRel of L1 : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( Relation-like the carrier of b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) = RelStr(# the carrier of L2 : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) , the InternalRel of L2 : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( Relation-like the carrier of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) -defined the carrier of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) -valued ) Element of bool [: the carrier of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) , the carrier of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) holds
xi L1 : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( ) Element of bool (bool the carrier of b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = xi L2 : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( ) Element of bool (bool the carrier of b₂ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

registration

let R be ( ( non empty reflexive /\-complete ) ( non empty reflexive lower-bounded /\-complete ) RelStr ) ;

cluster -> /\-complete for ( ( ) ( ) TopAugmentation of R : ( ( ) ( ) set ) ) ;

end;

registration

let R be ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima ) Semilattice) ;

cluster -> with_infima for ( ( ) ( ) TopAugmentation of R : ( ( ) ( ) set ) ) ;

end;

registration

let L be ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ;

cluster non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima strict lim-inf for ( ( ) ( ) TopAugmentation of L : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) RelStr ) ) ;

end;

theorem :: WAYBEL33:10

for L being ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice)
for X being ( ( lim-inf ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima lim-inf ) TopAugmentation of L : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) holds xi L : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( ) Element of bool (bool the carrier of b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = the topology of X : ( ( lim-inf ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima lim-inf ) TopAugmentation of b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( ) ( ) Element of bool (bool the carrier of b₂ : ( ( lim-inf ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima lim-inf ) TopAugmentation of b₁ : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

definition

let L be ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ;

func Xi L -> ( ( strict ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima strict ) TopAugmentation of L : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) RelStr ) ) means :: WAYBEL33:def 3
it : ( ( ) ( ) set ) is lim-inf ;

end;

registration

let L be ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) Semilattice) ;

cluster Xi L : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) RelStr ) : ( ( strict ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima strict ) TopAugmentation of L : ( ( reflexive transitive antisymmetric up-complete /\-complete with_infima ) ( non empty reflexive transitive antisymmetric lower-bounded up-complete /\-complete with_infima ) RelStr ) ) -> strict lim-inf ;

end;

theorem :: WAYBEL33:11

for L being ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE)
for N being ( ( non empty transitive directed ) ( non empty transitive directed ) net of L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) holds lim_inf N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) ) = "\/" ( { (inf (N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) | i : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty transitive strict directed ) subnet of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) ) where i is ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : verum } ,L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL33:12

for L being ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE)
for F being ( ( non empty proper filtered upper ) ( non empty proper filtered upper ) Filter of BoolePoset ([#] L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( non empty non proper directed filtered lower upper ) Element of bool the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete ) RelStr ) )
for f being ( ( ) ( ) Subset of ) st f : ( ( ) ( ) Subset of ) in F : ( ( non empty proper filtered upper ) ( non empty proper filtered upper ) Filter of BoolePoset ([#] b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( non empty non proper directed filtered lower upper ) Element of bool the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete ) RelStr ) ) holds
for i being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st i : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) `2 : ( ( ) ( ) set ) = f : ( ( ) ( ) Subset of ) holds
inf f : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) ) = inf ((a_net F : ( ( non empty proper filtered upper ) ( non empty proper filtered upper ) Filter of BoolePoset ([#] b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( non empty non proper directed filtered lower upper ) Element of bool the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete ) RelStr ) ) ) : ( ( non empty strict ) ( non empty reflexive transitive strict directed ) NetStr over b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) | i : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty reflexive transitive strict directed ) subnet of a_net b₂ : ( ( non empty proper filtered upper ) ( non empty proper filtered upper ) Filter of BoolePoset ([#] b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( non empty non proper directed filtered lower upper ) Element of bool the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete ) RelStr ) ) : ( ( non empty strict ) ( non empty reflexive transitive strict directed ) NetStr over b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL33:13

for L being ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE)
for F being ( ( non empty proper filtered upper ) ( non empty proper filtered upper ) Filter of BoolePoset ([#] L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( non empty non proper directed filtered lower upper ) Element of bool the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete ) RelStr ) ) holds lim_inf F : ( ( non empty proper filtered upper ) ( non empty proper filtered upper ) Filter of BoolePoset ([#] b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( non empty non proper directed filtered lower upper ) Element of bool the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete ) RelStr ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = lim_inf (a_net F : ( ( non empty proper filtered upper ) ( non empty proper filtered upper ) Filter of BoolePoset ([#] b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( non empty non proper directed filtered lower upper ) Element of bool the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete ) RelStr ) ) ) : ( ( non empty strict ) ( non empty reflexive transitive strict directed ) NetStr over b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL33:14

for L being ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE)
for F being ( ( non empty proper filtered upper ) ( non empty proper filtered upper ) Filter of BoolePoset ([#] L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( non empty non proper directed filtered lower upper ) Element of bool the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete ) RelStr ) ) holds a_net F : ( ( non empty proper filtered upper ) ( non empty proper filtered upper ) Filter of BoolePoset ([#] b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( non empty non proper directed filtered lower upper ) Element of bool the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete ) RelStr ) ) : ( ( non empty strict ) ( non empty reflexive transitive strict directed ) NetStr over b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) in NetUniv L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) ;

theorem :: WAYBEL33:15

for L being ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE)
for F being ( ( non empty filtered upper ultra ) ( non empty proper filtered upper ultra ) Filter of BoolePoset ([#] L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( non empty non proper directed filtered lower upper ) Element of bool the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete ) RelStr ) )
for p being ( ( Function-like V41( the carrier of (a_net b₂ : ( ( non empty filtered upper ultra ) ( non empty proper filtered upper ultra ) Filter of BoolePoset ([#] b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( non empty non proper directed filtered lower upper ) Element of bool the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete ) RelStr ) ) ) : ( ( non empty strict ) ( non empty reflexive transitive strict directed V266(b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) ) NetStr over b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( non empty ) set ) , the carrier of (a_net b₂ : ( ( non empty filtered upper ultra ) ( non empty proper filtered upper ultra ) Filter of BoolePoset ([#] b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( non empty non proper directed filtered lower upper ) Element of bool the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete ) RelStr ) ) ) : ( ( non empty strict ) ( non empty reflexive transitive strict directed V266(b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) ) NetStr over b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( non empty ) set ) ) greater_or_equal_to_id ) ( Relation-like the carrier of (a_net b₂ : ( ( non empty filtered upper ultra ) ( non empty proper filtered upper ultra ) Filter of BoolePoset ([#] b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( non empty non proper directed filtered lower upper ) Element of bool the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete ) RelStr ) ) ) : ( ( non empty strict ) ( non empty reflexive transitive strict directed V266(b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) ) NetStr over b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( non empty ) set ) -defined the carrier of (a_net b₂ : ( ( non empty filtered upper ultra ) ( non empty proper filtered upper ultra ) Filter of BoolePoset ([#] b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( non empty non proper directed filtered lower upper ) Element of bool the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete ) RelStr ) ) ) : ( ( non empty strict ) ( non empty reflexive transitive strict directed V266(b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) ) NetStr over b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( non empty ) set ) -valued Function-like V41( the carrier of (a_net b₂ : ( ( non empty filtered upper ultra ) ( non empty proper filtered upper ultra ) Filter of BoolePoset ([#] b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( non empty non proper directed filtered lower upper ) Element of bool the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete ) RelStr ) ) ) : ( ( non empty strict ) ( non empty reflexive transitive strict directed V266(b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) ) NetStr over b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( non empty ) set ) , the carrier of (a_net b₂ : ( ( non empty filtered upper ultra ) ( non empty proper filtered upper ultra ) Filter of BoolePoset ([#] b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( non empty non proper directed filtered lower upper ) Element of bool the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete ) RelStr ) ) ) : ( ( non empty strict ) ( non empty reflexive transitive strict directed V266(b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) ) NetStr over b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( non empty ) set ) ) greater_or_equal_to_id ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) holds lim_inf F : ( ( non empty filtered upper ultra ) ( non empty proper filtered upper ultra ) Filter of BoolePoset ([#] b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( non empty non proper directed filtered lower upper ) Element of bool the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete ) RelStr ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) >= inf ((a_net F : ( ( non empty filtered upper ultra ) ( non empty proper filtered upper ultra ) Filter of BoolePoset ([#] b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( non empty non proper directed filtered lower upper ) Element of bool the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete ) RelStr ) ) ) : ( ( non empty strict ) ( non empty reflexive transitive strict directed V266(b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) ) NetStr over b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) * p : ( ( Function-like V41( the carrier of (a_net b₂ : ( ( non empty filtered upper ultra ) ( non empty proper filtered upper ultra ) Filter of BoolePoset ([#] b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( non empty non proper directed filtered lower upper ) Element of bool the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete ) RelStr ) ) ) : ( ( non empty strict ) ( non empty reflexive transitive strict directed V266(b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) ) NetStr over b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( non empty ) set ) , the carrier of (a_net b₂ : ( ( non empty filtered upper ultra ) ( non empty proper filtered upper ultra ) Filter of BoolePoset ([#] b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( non empty non proper directed filtered lower upper ) Element of bool the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete ) RelStr ) ) ) : ( ( non empty strict ) ( non empty reflexive transitive strict directed V266(b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) ) NetStr over b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( non empty ) set ) ) greater_or_equal_to_id ) ( Relation-like the carrier of (a_net b₂ : ( ( non empty filtered upper ultra ) ( non empty proper filtered upper ultra ) Filter of BoolePoset ([#] b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( non empty non proper directed filtered lower upper ) Element of bool the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete ) RelStr ) ) ) : ( ( non empty strict ) ( non empty reflexive transitive strict directed V266(b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) ) NetStr over b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( non empty ) set ) -defined the carrier of (a_net b₂ : ( ( non empty filtered upper ultra ) ( non empty proper filtered upper ultra ) Filter of BoolePoset ([#] b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( non empty non proper directed filtered lower upper ) Element of bool the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete ) RelStr ) ) ) : ( ( non empty strict ) ( non empty reflexive transitive strict directed V266(b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) ) NetStr over b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( non empty ) set ) -valued Function-like V41( the carrier of (a_net b₂ : ( ( non empty filtered upper ultra ) ( non empty proper filtered upper ultra ) Filter of BoolePoset ([#] b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( non empty non proper directed filtered lower upper ) Element of bool the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete ) RelStr ) ) ) : ( ( non empty strict ) ( non empty reflexive transitive strict directed V266(b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) ) NetStr over b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( non empty ) set ) , the carrier of (a_net b₂ : ( ( non empty filtered upper ultra ) ( non empty proper filtered upper ultra ) Filter of BoolePoset ([#] b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( non empty non proper directed filtered lower upper ) Element of bool the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete ) RelStr ) ) ) : ( ( non empty strict ) ( non empty reflexive transitive strict directed V266(b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) ) NetStr over b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( non empty ) set ) ) greater_or_equal_to_id ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty transitive strict directed ) subnet of a_net b₂ : ( ( non empty filtered upper ultra ) ( non empty proper filtered upper ultra ) Filter of BoolePoset ([#] b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( non empty non proper directed filtered lower upper ) Element of bool the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete ) RelStr ) ) : ( ( non empty strict ) ( non empty reflexive transitive strict directed V266(b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) ) NetStr over b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL33:16

for L being ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE)
for F being ( ( non empty filtered upper ultra ) ( non empty proper filtered upper ultra ) Filter of BoolePoset ([#] L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( non empty non proper directed filtered lower upper ) Element of bool the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete ) RelStr ) )
for M being ( ( ) ( non empty transitive directed ) subnet of a_net F : ( ( non empty filtered upper ultra ) ( non empty proper filtered upper ultra ) Filter of BoolePoset ([#] b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( non empty non proper directed filtered lower upper ) Element of bool the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete ) RelStr ) ) : ( ( non empty strict ) ( non empty reflexive transitive strict directed V266(b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) ) NetStr over b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) ) holds lim_inf F : ( ( non empty filtered upper ultra ) ( non empty proper filtered upper ultra ) Filter of BoolePoset ([#] b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( non empty non proper directed filtered lower upper ) Element of bool the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete ) RelStr ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = lim_inf M : ( ( ) ( non empty transitive directed ) subnet of a_net b₂ : ( ( non empty filtered upper ultra ) ( non empty proper filtered upper ultra ) Filter of BoolePoset ([#] b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) : ( ( ) ( non empty non proper directed filtered lower upper ) Element of bool the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete ) RelStr ) ) : ( ( non empty strict ) ( non empty reflexive transitive strict directed V266(b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) ) NetStr over b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL33:17

for L being ( ( non empty ) ( non empty ) 1-sorted )
for N being ( ( non empty transitive directed ) ( non empty transitive directed ) net of L : ( ( non empty ) ( non empty ) 1-sorted ) )
for A being ( ( ) ( ) set ) st N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) is_often_in A : ( ( ) ( ) set ) holds
ex N9 being ( ( strict ) ( non empty transitive strict directed ) subnet of N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) ) st
( rng the mapping of N9 : ( ( strict ) ( non empty transitive strict directed ) subnet of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) ) : ( ( Function-like V41( the carrier of b₄ : ( ( strict ) ( non empty transitive strict directed ) subnet of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of b₄ : ( ( strict ) ( non empty transitive strict directed ) subnet of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V41( the carrier of b₄ : ( ( strict ) ( non empty transitive strict directed ) subnet of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) Element of bool [: the carrier of b₄ : ( ( strict ) ( non empty transitive strict directed ) subnet of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty Relation-like ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) c= A : ( ( ) ( ) set ) & N9 : ( ( strict ) ( non empty transitive strict directed ) subnet of b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) ) is ( ( ) ( ) SubNetStr of N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) 1-sorted ) ) ) ) ;

theorem :: WAYBEL33:18

for L being ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lim-inf ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lim-inf ) TopLattice)
for A being ( ( non empty ) ( non empty ) Subset of ) holds
( A : ( ( non empty ) ( non empty ) Subset of ) is closed iff for F being ( ( non empty filtered upper ultra ) ( non empty proper filtered upper ultra ) Filter of BoolePoset ([#] L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lim-inf ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lim-inf ) TopLattice) ) : ( ( ) ( non empty non proper open directed filtered lower upper ) Element of bool the carrier of b₁ : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lim-inf ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lim-inf ) TopLattice) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete ) RelStr ) ) st A : ( ( non empty ) ( non empty ) Subset of ) in F : ( ( non empty filtered upper ultra ) ( non empty proper filtered upper ultra ) Filter of BoolePoset ([#] b₁ : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lim-inf ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lim-inf ) TopLattice) ) : ( ( ) ( non empty non proper open directed filtered lower upper ) Element of bool the carrier of b₁ : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lim-inf ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lim-inf ) TopLattice) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete ) RelStr ) ) holds
lim_inf F : ( ( non empty filtered upper ultra ) ( non empty proper filtered upper ultra ) Filter of BoolePoset ([#] b₁ : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lim-inf ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lim-inf ) TopLattice) ) : ( ( ) ( non empty non proper open directed filtered lower upper ) Element of bool the carrier of b₁ : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lim-inf ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lim-inf ) TopLattice) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete ) RelStr ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in A : ( ( non empty ) ( non empty ) Subset of ) ) ;

theorem :: WAYBEL33:19

for L being ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) holds sigma L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( ) Element of bool (bool the carrier of b₁ : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) c= xi L : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( ) Element of bool (bool the carrier of b₁ : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL33:20

for T1, T2 being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for B being ( ( quasi_prebasis V269(b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) ) ( quasi_prebasis V269(b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) ) prebasis of T1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) st B : ( ( quasi_prebasis V269(b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) ) ( quasi_prebasis V269(b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) ) prebasis of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ) c= the topology of T2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) Element of bool (bool the carrier of b₂ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) & the carrier of T1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) in the topology of T2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) Element of bool (bool the carrier of b₂ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) holds
the topology of T1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) Element of bool (bool the carrier of b₁ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) c= the topology of T2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( ) Element of bool (bool the carrier of b₂ : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL33:21

for L being ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) holds omega L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( ) Element of bool (bool the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) c= xi L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( ) Element of bool (bool the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL33:22

for T1, T2 being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) st T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is ( ( ) ( TopSpace-like ) TopExtension of T1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) & T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is ( ( ) ( TopSpace-like ) TopExtension of T2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) holds
for R being ( ( ) ( TopSpace-like ) Refinement of T1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ,T2 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) holds T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) is ( ( ) ( TopSpace-like ) TopExtension of R : ( ( ) ( TopSpace-like ) Refinement of b₁ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ,b₂ : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) ) ) ;

theorem :: WAYBEL33:23

for T1 being ( ( TopSpace-like ) ( TopSpace-like ) TopSpace)
for T2 being ( ( ) ( TopSpace-like ) TopExtension of T1 : ( ( TopSpace-like ) ( TopSpace-like ) TopSpace) )
for A being ( ( ) ( ) Subset of ) holds
( ( A : ( ( ) ( ) Subset of ) is open implies A : ( ( ) ( ) Subset of ) is ( ( open ) ( open ) Subset of ) ) & ( A : ( ( ) ( ) Subset of ) is closed implies A : ( ( ) ( ) Subset of ) is ( ( closed ) ( closed ) Subset of ) ) ) ;

theorem :: WAYBEL33:24

for L being ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) holds lambda L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( ) Element of bool (bool the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) c= xi L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( ) Element of bool (bool the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL33:25

for L being ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE)
for T being ( ( lim-inf ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lim-inf ) TopAugmentation of L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) )
for S being ( ( correct Lawson ) ( non empty correct T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete Lawson compact ) TopAugmentation of L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) holds T : ( ( lim-inf ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lim-inf ) TopAugmentation of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) is ( ( ) ( TopSpace-like ) TopExtension of S : ( ( correct Lawson ) ( non empty correct T_1 reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete Lawson compact ) TopAugmentation of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ) ) ;

theorem :: WAYBEL33:26

for L being ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lim-inf ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lim-inf ) TopLattice)
for F being ( ( non empty filtered upper ultra ) ( non empty proper filtered upper ultra ) Filter of BoolePoset ([#] L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lim-inf ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lim-inf ) TopLattice) ) : ( ( ) ( non empty non proper open directed filtered lower upper ) Element of bool the carrier of b₁ : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lim-inf ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lim-inf ) TopLattice) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete ) RelStr ) ) holds lim_inf F : ( ( non empty filtered upper ultra ) ( non empty proper filtered upper ultra ) Filter of BoolePoset ([#] b₁ : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lim-inf ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lim-inf ) TopLattice) ) : ( ( ) ( non empty non proper open directed filtered lower upper ) Element of bool the carrier of b₁ : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lim-inf ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lim-inf ) TopLattice) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete ) RelStr ) ) : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is_a_convergence_point_of F : ( ( non empty filtered upper ultra ) ( non empty proper filtered upper ultra ) Filter of BoolePoset ([#] b₁ : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lim-inf ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lim-inf ) TopLattice) ) : ( ( ) ( non empty non proper open directed filtered lower upper ) Element of bool the carrier of b₁ : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lim-inf ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lim-inf ) TopLattice) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V163() directed up-complete /\-complete V205() with_suprema with_infima complete ) RelStr ) ) ,L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lim-inf ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lim-inf ) TopLattice) ;

theorem :: WAYBEL33:27

for L being ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lim-inf ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lim-inf ) TopLattice) holds
( L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lim-inf ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lim-inf ) TopLattice) is compact & L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lim-inf ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V163() up-complete /\-complete with_suprema with_infima complete lim-inf ) TopLattice) is T_1 ) ;