WAYBEL32

:: WAYBEL32 semantic presentation

begin

definition

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

attr T is upper means :: WAYBEL32:def 1
{ ((downarrow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool the carrier of T : ( ( ) ( ) TopRelStr ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( ) Element of bool the carrier of T : ( ( ) ( ) TopRelStr ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) where x is ( ( ) ( ) Element of ( ( ) ( ) set ) ) : verum } is ( ( V69(T : ( ( ) ( ) TopRelStr ) ) quasi_prebasis ) ( V69(T : ( ( ) ( ) TopRelStr ) ) quasi_prebasis ) prebasis of T : ( ( ) ( ) TopRelStr ) ) ;

end;

registration

cluster non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima up-complete strict Scott for ( ( ) ( ) TopRelStr ) ;

end;

definition

let T be ( ( non empty TopSpace-like reflexive ) ( non empty TopSpace-like reflexive ) TopRelStr ) ;

attr T is order_consistent means :: WAYBEL32:def 2
for x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
( downarrow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of T : ( ( ) ( ) TopRelStr ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = Cl {x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty trivial V35(1 : ( ( ) ( non empty ) set ) ) ) Element of bool the carrier of T : ( ( ) ( ) TopRelStr ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of T : ( ( ) ( ) TopRelStr ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) & ( for N being ( ( non empty transitive directed eventually-directed ) ( non empty transitive directed eventually-directed ) net of T : ( ( ) ( ) TopRelStr ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = sup N : ( ( non empty transitive directed eventually-directed ) ( non empty transitive directed eventually-directed ) net of T : ( ( non empty TopSpace-like reflexive ) ( non empty TopSpace-like reflexive ) TopRelStr ) ) : ( ( ) ( ) Element of the carrier of T : ( ( ) ( ) TopRelStr ) : ( ( ) ( ) set ) ) holds
for V being ( ( ) ( ) a_neighborhood of x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) holds N : ( ( non empty transitive directed eventually-directed ) ( non empty transitive directed eventually-directed ) net of T : ( ( non empty TopSpace-like reflexive ) ( non empty TopSpace-like reflexive ) TopRelStr ) ) is_eventually_in V : ( ( ) ( ) a_neighborhood of b₁ : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) );

end;

registration

cluster 1 : ( ( ) ( non empty ) set ) -element TopSpace-like reflexive -> 1 : ( ( ) ( non empty ) set ) -element TopSpace-like reflexive upper for ( ( ) ( ) TopRelStr ) ;

end;

registration

cluster non empty trivial TopSpace-like reflexive transitive antisymmetric with_suprema with_infima up-complete strict upper for ( ( ) ( ) TopRelStr ) ;

end;

theorem :: WAYBEL32:1

for T being ( ( non empty TopSpace-like reflexive transitive antisymmetric up-complete upper ) ( non empty TopSpace-like reflexive transitive antisymmetric up-complete upper ) TopPoset)
for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is open holds
A : ( ( ) ( ) Subset of ) is upper ;

theorem :: WAYBEL32:2

for T being ( ( non empty TopSpace-like reflexive transitive antisymmetric up-complete ) ( non empty TopSpace-like reflexive transitive antisymmetric up-complete ) TopPoset) st T : ( ( non empty TopSpace-like reflexive transitive antisymmetric up-complete ) ( non empty TopSpace-like reflexive transitive antisymmetric up-complete ) TopPoset) is upper holds
T : ( ( non empty TopSpace-like reflexive transitive antisymmetric up-complete ) ( non empty TopSpace-like reflexive transitive antisymmetric up-complete ) TopPoset) is order_consistent ;

theorem :: WAYBEL32:3

for R being ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) ex T being ( ( ) ( non empty reflexive transitive antisymmetric up-complete ) TopAugmentation of R : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) ) st T : ( ( ) ( non empty reflexive transitive antisymmetric up-complete ) TopAugmentation of b₁ : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) ) is Scott ;

theorem :: WAYBEL32:4

for R being ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) Poset)
for T being ( ( ) ( non empty reflexive transitive antisymmetric up-complete ) TopAugmentation of R : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) Poset) ) st T : ( ( ) ( non empty reflexive transitive antisymmetric up-complete ) TopAugmentation of b₁ : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) Poset) ) is Scott holds
T : ( ( ) ( non empty reflexive transitive antisymmetric up-complete ) TopAugmentation of b₁ : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) Poset) ) is correct ;

registration

let R be ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) ;

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

end;

registration

let R be ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) ;

cluster non empty correct reflexive transitive antisymmetric up-complete Scott for ( ( ) ( ) TopAugmentation of R : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) ) ;

end;

theorem :: WAYBEL32:5

for T being ( ( non empty reflexive transitive antisymmetric up-complete Scott ) ( non empty reflexive transitive antisymmetric up-complete Scott ) TopRelStr )
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds Cl {x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty trivial V35(1 : ( ( ) ( non empty ) set ) ) ) Element of bool the carrier of b₁ : ( ( non empty reflexive transitive antisymmetric up-complete Scott ) ( non empty reflexive transitive antisymmetric up-complete Scott ) TopRelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( non empty reflexive transitive antisymmetric up-complete Scott ) ( non empty reflexive transitive antisymmetric up-complete Scott ) TopRelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = downarrow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty directed lower ) Element of bool the carrier of b₁ : ( ( non empty reflexive transitive antisymmetric up-complete Scott ) ( non empty reflexive transitive antisymmetric up-complete Scott ) TopRelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL32:6

for T being ( ( non empty TopSpace-like reflexive transitive antisymmetric up-complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric up-complete Scott ) TopPoset) holds T : ( ( non empty TopSpace-like reflexive transitive antisymmetric up-complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric up-complete Scott ) TopPoset) is order_consistent ;

theorem :: WAYBEL32:7

for R being ( ( reflexive transitive antisymmetric with_infima /\-complete ) ( non empty reflexive transitive antisymmetric with_infima lower-bounded /\-complete ) Semilattice)
for Z being ( ( non empty transitive directed ) ( non empty transitive directed ) net of R : ( ( reflexive transitive antisymmetric with_infima /\-complete ) ( non empty reflexive transitive antisymmetric with_infima lower-bounded /\-complete ) Semilattice) )
for D being ( ( ) ( ) Subset of ) st D : ( ( ) ( ) Subset of ) = { ("/\" ( { (Z : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( reflexive transitive antisymmetric with_infima /\-complete ) ( non empty reflexive transitive antisymmetric with_infima lower-bounded /\-complete ) Semilattice) ) . k : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( reflexive transitive antisymmetric with_infima /\-complete ) ( non empty reflexive transitive antisymmetric with_infima lower-bounded /\-complete ) Semilattice) : ( ( ) ( non empty ) set ) ) where k is ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : k : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) >= j : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) } ,R : ( ( reflexive transitive antisymmetric with_infima /\-complete ) ( non empty reflexive transitive antisymmetric with_infima lower-bounded /\-complete ) Semilattice) )) : ( ( ) ( ) Element of the carrier of b₁ : ( ( reflexive transitive antisymmetric with_infima /\-complete ) ( non empty reflexive transitive antisymmetric with_infima lower-bounded /\-complete ) Semilattice) : ( ( ) ( non empty ) set ) ) where j is ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : verum } holds
( not D : ( ( ) ( ) Subset of ) is empty & D : ( ( ) ( ) Subset of ) is directed ) ;

theorem :: WAYBEL32:8

for R being ( ( reflexive transitive antisymmetric with_infima /\-complete ) ( non empty reflexive transitive antisymmetric with_infima lower-bounded /\-complete ) Semilattice)
for S being ( ( ) ( ) Subset of )
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in S : ( ( ) ( ) Subset of ) holds
"/\" (S : ( ( ) ( ) Subset of ) ,R : ( ( reflexive transitive antisymmetric with_infima /\-complete ) ( non empty reflexive transitive antisymmetric with_infima lower-bounded /\-complete ) Semilattice) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( reflexive transitive antisymmetric with_infima /\-complete ) ( non empty reflexive transitive antisymmetric with_infima lower-bounded /\-complete ) Semilattice) : ( ( ) ( non empty ) set ) ) <= a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL32:9

for R being ( ( reflexive transitive antisymmetric with_infima /\-complete ) ( non empty reflexive transitive antisymmetric with_infima lower-bounded /\-complete ) Semilattice)
for N being ( ( non empty reflexive transitive directed monotone ) ( non empty reflexive transitive directed monotone eventually-directed ) net of R : ( ( reflexive transitive antisymmetric with_infima /\-complete ) ( non empty reflexive transitive antisymmetric with_infima lower-bounded /\-complete ) Semilattice) ) holds lim_inf N : ( ( non empty reflexive transitive directed monotone ) ( non empty reflexive transitive directed monotone eventually-directed ) net of b₁ : ( ( reflexive transitive antisymmetric with_infima /\-complete ) ( non empty reflexive transitive antisymmetric with_infima lower-bounded /\-complete ) Semilattice) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( reflexive transitive antisymmetric with_infima /\-complete ) ( non empty reflexive transitive antisymmetric with_infima lower-bounded /\-complete ) Semilattice) : ( ( ) ( non empty ) set ) ) = sup N : ( ( non empty reflexive transitive directed monotone ) ( non empty reflexive transitive directed monotone eventually-directed ) net of b₁ : ( ( reflexive transitive antisymmetric with_infima /\-complete ) ( non empty reflexive transitive antisymmetric with_infima lower-bounded /\-complete ) Semilattice) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( reflexive transitive antisymmetric with_infima /\-complete ) ( non empty reflexive transitive antisymmetric with_infima lower-bounded /\-complete ) Semilattice) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL32:10

for R being ( ( reflexive transitive antisymmetric with_infima /\-complete ) ( non empty reflexive transitive antisymmetric with_infima lower-bounded /\-complete ) Semilattice)
for S being ( ( ) ( ) Subset of ) holds
( S : ( ( ) ( ) Subset of ) in the topology of (ConvergenceSpace (Scott-Convergence R : ( ( reflexive transitive antisymmetric with_infima /\-complete ) ( non empty reflexive transitive antisymmetric with_infima lower-bounded /\-complete ) Semilattice) ) : ( ( ) ( Relation-like ) Convergence-Class of b₁ : ( ( reflexive transitive antisymmetric with_infima /\-complete ) ( non empty reflexive transitive antisymmetric with_infima lower-bounded /\-complete ) Semilattice) ) ) : ( ( strict ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( ) Element of bool (bool the carrier of (ConvergenceSpace (Scott-Convergence b₁ : ( ( reflexive transitive antisymmetric with_infima /\-complete ) ( non empty reflexive transitive antisymmetric with_infima lower-bounded /\-complete ) Semilattice) ) : ( ( ) ( Relation-like ) Convergence-Class of b₁ : ( ( reflexive transitive antisymmetric with_infima /\-complete ) ( non empty reflexive transitive antisymmetric with_infima lower-bounded /\-complete ) Semilattice) ) ) : ( ( strict ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) iff ( S : ( ( ) ( ) Subset of ) is inaccessible & S : ( ( ) ( ) Subset of ) is upper ) ) ;

theorem :: WAYBEL32:11

for R being ( ( reflexive transitive antisymmetric with_infima up-complete /\-complete ) ( non empty reflexive transitive antisymmetric with_infima lower-bounded up-complete /\-complete ) Semilattice)
for T being ( ( ) ( non empty reflexive transitive antisymmetric up-complete ) TopAugmentation of R : ( ( reflexive transitive antisymmetric with_infima up-complete /\-complete ) ( non empty reflexive transitive antisymmetric with_infima lower-bounded up-complete /\-complete ) Semilattice) ) st the topology of T : ( ( ) ( non empty reflexive transitive antisymmetric up-complete ) TopAugmentation of b₁ : ( ( reflexive transitive antisymmetric with_infima up-complete /\-complete ) ( non empty reflexive transitive antisymmetric with_infima lower-bounded up-complete /\-complete ) Semilattice) ) : ( ( ) ( ) Element of bool (bool the carrier of b₂ : ( ( ) ( non empty reflexive transitive antisymmetric up-complete ) TopAugmentation of b₁ : ( ( reflexive transitive antisymmetric with_infima up-complete /\-complete ) ( non empty reflexive transitive antisymmetric with_infima lower-bounded up-complete /\-complete ) Semilattice) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = sigma R : ( ( reflexive transitive antisymmetric with_infima up-complete /\-complete ) ( non empty reflexive transitive antisymmetric with_infima lower-bounded up-complete /\-complete ) Semilattice) : ( ( ) ( ) Element of bool (bool the carrier of b₁ : ( ( reflexive transitive antisymmetric with_infima up-complete /\-complete ) ( non empty reflexive transitive antisymmetric with_infima lower-bounded up-complete /\-complete ) Semilattice) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) holds
T : ( ( ) ( non empty reflexive transitive antisymmetric up-complete ) TopAugmentation of b₁ : ( ( reflexive transitive antisymmetric with_infima up-complete /\-complete ) ( non empty reflexive transitive antisymmetric with_infima lower-bounded up-complete /\-complete ) Semilattice) ) is Scott ;

registration

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

cluster non empty correct reflexive transitive antisymmetric up-complete strict Scott for ( ( ) ( ) TopAugmentation of R : ( ( reflexive transitive antisymmetric with_infima up-complete /\-complete ) ( non empty reflexive transitive antisymmetric with_infima lower-bounded up-complete /\-complete ) RelStr ) ) ;

end;

theorem :: WAYBEL32:12

for S being ( ( reflexive transitive antisymmetric with_infima up-complete /\-complete ) ( non empty reflexive transitive antisymmetric with_infima lower-bounded up-complete /\-complete ) Semilattice)
for T being ( ( Scott ) ( non empty correct reflexive transitive antisymmetric up-complete Scott ) TopAugmentation of S : ( ( reflexive transitive antisymmetric with_infima up-complete /\-complete ) ( non empty reflexive transitive antisymmetric with_infima lower-bounded up-complete /\-complete ) Semilattice) ) holds sigma S : ( ( reflexive transitive antisymmetric with_infima up-complete /\-complete ) ( non empty reflexive transitive antisymmetric with_infima lower-bounded up-complete /\-complete ) Semilattice) : ( ( ) ( ) Element of bool (bool the carrier of b₁ : ( ( reflexive transitive antisymmetric with_infima up-complete /\-complete ) ( non empty reflexive transitive antisymmetric with_infima lower-bounded up-complete /\-complete ) Semilattice) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = the topology of T : ( ( Scott ) ( non empty correct reflexive transitive antisymmetric up-complete Scott ) TopAugmentation of b₁ : ( ( reflexive transitive antisymmetric with_infima up-complete /\-complete ) ( non empty reflexive transitive antisymmetric with_infima lower-bounded up-complete /\-complete ) Semilattice) ) : ( ( ) ( ) Element of bool (bool the carrier of b₂ : ( ( Scott ) ( non empty correct reflexive transitive antisymmetric up-complete Scott ) TopAugmentation of b₁ : ( ( reflexive transitive antisymmetric with_infima up-complete /\-complete ) ( non empty reflexive transitive antisymmetric with_infima lower-bounded up-complete /\-complete ) Semilattice) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL32:13

for T being ( ( non empty reflexive transitive antisymmetric up-complete Scott ) ( non empty reflexive transitive antisymmetric up-complete Scott ) TopRelStr ) holds T : ( ( non empty reflexive transitive antisymmetric up-complete Scott ) ( non empty reflexive transitive antisymmetric up-complete Scott ) TopRelStr ) is ( ( non empty TopSpace-like T_0 ) ( non empty TopSpace-like T_0 ) T_0-TopSpace) ;

registration

let R be ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) ;

cluster -> up-complete for ( ( ) ( ) TopAugmentation of R : ( ( reflexive transitive antisymmetric with_infima up-complete /\-complete ) ( non empty reflexive transitive antisymmetric with_infima lower-bounded up-complete /\-complete ) RelStr ) ) ;

end;

theorem :: WAYBEL32:14

for R being ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr )
for T being ( ( Scott ) ( non empty correct reflexive transitive antisymmetric up-complete Scott ) TopAugmentation of R : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) )
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for A being ( ( upper ) ( upper ) Subset of ) st not x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in A : ( ( upper ) ( upper ) Subset of ) holds
(downarrow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty directed lower ) Element of bool the carrier of b₂ : ( ( Scott ) ( non empty correct reflexive transitive antisymmetric up-complete Scott ) TopAugmentation of b₁ : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ` : ( ( ) ( upper ) Element of bool the carrier of b₂ : ( ( Scott ) ( non empty correct reflexive transitive antisymmetric up-complete Scott ) TopAugmentation of b₁ : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is ( ( ) ( ) a_neighborhood of A : ( ( upper ) ( upper ) Subset of ) ) ;

theorem :: WAYBEL32:15

for R being ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) TopRelStr )
for T being ( ( Scott ) ( non empty correct reflexive transitive antisymmetric up-complete Scott ) TopAugmentation of R : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) TopRelStr ) )
for S being ( ( upper ) ( upper ) Subset of ) ex F being ( ( ) ( ) Subset-Family of ) st
( S : ( ( upper ) ( upper ) Subset of ) = meet F : ( ( ) ( ) Subset-Family of ) : ( ( ) ( ) Element of bool the carrier of b₂ : ( ( Scott ) ( non empty correct reflexive transitive antisymmetric up-complete Scott ) TopAugmentation of b₁ : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) TopRelStr ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) & ( for X being ( ( ) ( ) Subset of ) st X : ( ( ) ( ) Subset of ) in F : ( ( ) ( ) Subset-Family of ) holds
X : ( ( ) ( ) Subset of ) is ( ( ) ( ) a_neighborhood of S : ( ( upper ) ( upper ) Subset of ) ) ) ) ;

theorem :: WAYBEL32:16

for T being ( ( non empty reflexive transitive antisymmetric up-complete Scott ) ( non empty reflexive transitive antisymmetric up-complete Scott ) TopRelStr )
for S being ( ( ) ( ) Subset of ) holds
( S : ( ( ) ( ) Subset of ) is open iff ( S : ( ( ) ( ) Subset of ) is upper & S : ( ( ) ( ) Subset of ) is property(S) ) ) ;

theorem :: WAYBEL32:17

for R being ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) TopRelStr )
for S being ( ( non empty directed ) ( non empty directed ) Subset of )
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in S : ( ( non empty directed ) ( non empty directed ) Subset of ) holds
a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= "\/" (S : ( ( non empty directed ) ( non empty directed ) Subset of ) ,R : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) TopRelStr ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) TopRelStr ) : ( ( ) ( non empty ) set ) ) ;

registration

let T be ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) TopRelStr ) ;

cluster lower -> property(S) for ( ( ) ( ) Element of bool the carrier of T : ( ( reflexive transitive antisymmetric with_infima up-complete /\-complete ) ( non empty reflexive transitive antisymmetric with_infima lower-bounded up-complete /\-complete ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

end;

theorem :: WAYBEL32:18

for T being ( ( non empty finite reflexive transitive antisymmetric up-complete ) ( non empty finite reflexive transitive antisymmetric up-complete ) Poset)
for S being ( ( ) ( finite ) Subset of ) holds S : ( ( ) ( finite ) Subset of ) is inaccessible ;

theorem :: WAYBEL32:19

for R being ( ( reflexive transitive antisymmetric with_suprema with_infima complete connected ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() connected up-complete /\-complete ) LATTICE)
for T being ( ( Scott ) ( non empty correct reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() up-complete /\-complete Scott ) TopAugmentation of R : ( ( reflexive transitive antisymmetric with_suprema with_infima complete connected ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() connected up-complete /\-complete ) LATTICE) )
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds (downarrow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty directed lower property(S) ) Element of bool the carrier of b₂ : ( ( Scott ) ( non empty correct reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() up-complete /\-complete Scott ) TopAugmentation of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete connected ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() connected up-complete /\-complete ) LATTICE) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ` : ( ( ) ( upper closed_under_directed_sups ) Element of bool the carrier of b₂ : ( ( Scott ) ( non empty correct reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() up-complete /\-complete Scott ) TopAugmentation of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete connected ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() connected up-complete /\-complete ) LATTICE) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is open ;

theorem :: WAYBEL32:20

for R being ( ( reflexive transitive antisymmetric with_suprema with_infima complete connected ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() connected up-complete /\-complete ) LATTICE)
for T being ( ( Scott ) ( non empty correct reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() up-complete /\-complete Scott ) TopAugmentation of R : ( ( reflexive transitive antisymmetric with_suprema with_infima complete connected ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() connected up-complete /\-complete ) LATTICE) )
for S being ( ( ) ( ) Subset of ) holds
( S : ( ( ) ( ) Subset of ) is open iff ( S : ( ( ) ( ) Subset of ) = the carrier of T : ( ( Scott ) ( non empty correct reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() up-complete /\-complete Scott ) TopAugmentation of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete connected ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() connected up-complete /\-complete ) LATTICE) ) : ( ( ) ( non empty ) set ) or S : ( ( ) ( ) Subset of ) in { ((downarrow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty directed lower property(S) ) Element of bool the carrier of b₂ : ( ( Scott ) ( non empty correct reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() up-complete /\-complete Scott ) TopAugmentation of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete connected ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() connected up-complete /\-complete ) LATTICE) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( upper closed_under_directed_sups ) Element of bool the carrier of b₂ : ( ( Scott ) ( non empty correct reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() up-complete /\-complete Scott ) TopAugmentation of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima complete connected ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() connected up-complete /\-complete ) LATTICE) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) where x is ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : verum } ) ) ;

registration

let R be ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) Poset) ;

cluster non empty correct reflexive transitive antisymmetric up-complete order_consistent for ( ( ) ( ) TopAugmentation of R : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) ) ;

end;

registration

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

end;

theorem :: WAYBEL32:21

for R being ( ( non empty ) ( non empty ) TopRelStr )
for A being ( ( ) ( ) Subset of ) st ( for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds downarrow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( non empty ) ( non empty ) TopRelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = Cl {x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty trivial V35(1 : ( ( ) ( non empty ) set ) ) ) Element of bool the carrier of b₁ : ( ( non empty ) ( non empty ) TopRelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( non empty ) ( non empty ) TopRelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) & A : ( ( ) ( ) Subset of ) is open holds
A : ( ( ) ( ) Subset of ) is upper ;

theorem :: WAYBEL32:22

for R being ( ( non empty ) ( non empty ) TopRelStr )
for A being ( ( ) ( ) Subset of ) st ( for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds downarrow x : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( non empty ) ( non empty ) TopRelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = Cl {x : ( ( ) ( ) Subset of ) } : ( ( ) ( non empty trivial V35(1 : ( ( ) ( non empty ) set ) ) ) Element of bool the carrier of b₁ : ( ( non empty ) ( non empty ) TopRelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b₁ : ( ( non empty ) ( non empty ) TopRelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) holds
for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) is closed holds
A : ( ( ) ( ) Subset of ) is lower ;

definition

let S be ( ( non empty ) ( non empty ) 1-sorted ) ;
let R be ( ( non empty ) ( non empty ) RelStr ) ;
let f be ( ( Function-like V18( the carrier of R : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of R : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of R : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) Function of the carrier of R : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ;

func R *' f -> ( ( non empty strict ) ( non empty strict ) NetStr over S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) ) means :: WAYBEL32:def 3
( RelStr(# the carrier of it : ( ( Function-like V18(R : ( ( ) ( ) set ) , the carrier of S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like R : ( ( ) ( ) set ) -defined the carrier of S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18(R : ( ( ) ( ) set ) , the carrier of S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Element of bool [:R : ( ( ) ( ) set ) , the carrier of S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) , the InternalRel of it : ( ( Function-like V18(R : ( ( ) ( ) set ) , the carrier of S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like R : ( ( ) ( ) set ) -defined the carrier of S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18(R : ( ( ) ( ) set ) , the carrier of S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Element of bool [:R : ( ( ) ( ) set ) , the carrier of S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( Relation-like the carrier of it : ( ( Function-like V18(R : ( ( ) ( ) set ) , the carrier of S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like R : ( ( ) ( ) set ) -defined the carrier of S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18(R : ( ( ) ( ) set ) , the carrier of S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Element of bool [:R : ( ( ) ( ) set ) , the carrier of S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) -defined the carrier of it : ( ( Function-like V18(R : ( ( ) ( ) set ) , the carrier of S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like R : ( ( ) ( ) set ) -defined the carrier of S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18(R : ( ( ) ( ) set ) , the carrier of S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Element of bool [:R : ( ( ) ( ) set ) , the carrier of S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued ) Element of bool [: the carrier of it : ( ( Function-like V18(R : ( ( ) ( ) set ) , the carrier of S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like R : ( ( ) ( ) set ) -defined the carrier of S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18(R : ( ( ) ( ) set ) , the carrier of S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Element of bool [:R : ( ( ) ( ) set ) , the carrier of S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( Function-like V18(R : ( ( ) ( ) set ) , the carrier of S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like R : ( ( ) ( ) set ) -defined the carrier of S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18(R : ( ( ) ( ) set ) , the carrier of S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Element of bool [:R : ( ( ) ( ) set ) , the carrier of S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) = RelStr(# the carrier of R : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the InternalRel of R : ( ( ) ( ) set ) : ( ( ) ( Relation-like the carrier of R : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of R : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued ) Element of bool [: the carrier of R : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of R : ( ( ) ( ) set ) : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( strict ) RelStr ) & the mapping of it : ( ( Function-like V18(R : ( ( ) ( ) set ) , the carrier of S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like R : ( ( ) ( ) set ) -defined the carrier of S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18(R : ( ( ) ( ) set ) , the carrier of S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Element of bool [:R : ( ( ) ( ) set ) , the carrier of S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like V18( the carrier of it : ( ( Function-like V18(R : ( ( ) ( ) set ) , the carrier of S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like R : ( ( ) ( ) set ) -defined the carrier of S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18(R : ( ( ) ( ) set ) , the carrier of S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Element of bool [:R : ( ( ) ( ) set ) , the carrier of S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) , the carrier of S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of it : ( ( Function-like V18(R : ( ( ) ( ) set ) , the carrier of S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like R : ( ( ) ( ) set ) -defined the carrier of S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18(R : ( ( ) ( ) set ) , the carrier of S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Element of bool [:R : ( ( ) ( ) set ) , the carrier of S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) -defined the carrier of S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of it : ( ( Function-like V18(R : ( ( ) ( ) set ) , the carrier of S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like R : ( ( ) ( ) set ) -defined the carrier of S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18(R : ( ( ) ( ) set ) , the carrier of S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Element of bool [:R : ( ( ) ( ) set ) , the carrier of S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) , the carrier of S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Element of bool [: the carrier of it : ( ( Function-like V18(R : ( ( ) ( ) set ) , the carrier of S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like R : ( ( ) ( ) set ) -defined the carrier of S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18(R : ( ( ) ( ) set ) , the carrier of S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Element of bool [:R : ( ( ) ( ) set ) , the carrier of S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) , the carrier of S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = f : ( ( ) ( ) Element of bool (bool S : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) );

end;

registration

let S be ( ( non empty ) ( non empty ) 1-sorted ) ;
let R be ( ( non empty transitive ) ( non empty transitive ) RelStr ) ;
let f be ( ( Function-like V18( the carrier of R : ( ( non empty transitive ) ( non empty transitive ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of R : ( ( non empty transitive ) ( non empty transitive ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of R : ( ( non empty transitive ) ( non empty transitive ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) Function of the carrier of R : ( ( non empty transitive ) ( non empty transitive ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ;

cluster R : ( ( non empty transitive ) ( non empty transitive ) RelStr ) *' f : ( ( Function-like V18( the carrier of R : ( ( non empty transitive ) ( non empty transitive ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of R : ( ( non empty transitive ) ( non empty transitive ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of R : ( ( non empty transitive ) ( non empty transitive ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) Element of bool [: the carrier of R : ( ( non empty transitive ) ( non empty transitive ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( non empty strict ) ( non empty strict ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) -> non empty transitive strict ;

end;

registration

let S be ( ( non empty ) ( non empty ) 1-sorted ) ;
let R be ( ( non empty directed ) ( non empty directed ) RelStr ) ;
let f be ( ( Function-like V18( the carrier of R : ( ( non empty directed ) ( non empty directed ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of R : ( ( non empty directed ) ( non empty directed ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of R : ( ( non empty directed ) ( non empty directed ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) Function of the carrier of R : ( ( non empty directed ) ( non empty directed ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ;

cluster R : ( ( non empty directed ) ( non empty directed ) RelStr ) *' f : ( ( Function-like V18( the carrier of R : ( ( non empty directed ) ( non empty directed ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of R : ( ( non empty directed ) ( non empty directed ) RelStr ) : ( ( ) ( non empty ) set ) -defined the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of R : ( ( non empty directed ) ( non empty directed ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) ) ) Element of bool [: the carrier of R : ( ( non empty directed ) ( non empty directed ) RelStr ) : ( ( ) ( non empty ) set ) , the carrier of S : ( ( non empty ) ( non empty ) 1-sorted ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( non empty strict ) ( non empty strict ) NetStr over S : ( ( non empty ) ( non empty ) 1-sorted ) ) -> non empty strict directed ;

end;

definition

let R be ( ( non empty ) ( non empty ) RelStr ) ;
let N be ( ( non empty directed ) ( non empty directed ) prenet of R : ( ( non empty ) ( non empty ) RelStr ) ) ;

func inf_net N -> ( ( non empty strict directed ) ( non empty strict directed ) prenet of R : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) ) means :: WAYBEL32:def 4
ex f being ( ( Function-like V18( the carrier of N : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of R : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of N : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of R : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of N : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of R : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) st
( it : ( ( Function-like V18( the carrier of N : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of R : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of N : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of R : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of N : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of R : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Element of bool [: the carrier of N : ( ( ) ( ) set ) : ( ( ) ( ) set ) , the carrier of R : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = N : ( ( ) ( ) set ) *' f : ( ( Function-like V18( the carrier of N : ( ( non empty directed ) ( non empty directed ) prenet of R : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( ) ( non empty ) set ) , the carrier of R : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of N : ( ( non empty directed ) ( non empty directed ) prenet of R : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( ) ( non empty ) set ) -defined the carrier of R : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of N : ( ( non empty directed ) ( non empty directed ) prenet of R : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( ) ( non empty ) set ) , the carrier of R : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) : ( ( non empty strict ) ( non empty strict ) NetStr over R : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) ) & ( for i being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds f : ( ( Function-like V18( the carrier of N : ( ( non empty directed ) ( non empty directed ) prenet of R : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( ) ( non empty ) set ) , the carrier of R : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of N : ( ( non empty directed ) ( non empty directed ) prenet of R : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( ) ( non empty ) set ) -defined the carrier of R : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of N : ( ( non empty directed ) ( non empty directed ) prenet of R : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( ) ( non empty ) set ) , the carrier of R : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) . i : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of R : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) ) = "/\" ( { (N : ( ( ) ( ) set ) . k : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of R : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) ) where k is ( ( ) ( ) Element of ( ( ) ( ) set ) ) : k : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) >= i : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) } ,R : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) ) : ( ( ) ( ) Element of the carrier of R : ( ( non empty reflexive transitive antisymmetric up-complete ) ( non empty reflexive transitive antisymmetric up-complete ) RelStr ) : ( ( ) ( non empty ) set ) ) ) );

end;

registration

let R be ( ( non empty ) ( non empty ) RelStr ) ;
let N be ( ( non empty transitive directed ) ( non empty transitive directed ) net of R : ( ( non empty ) ( non empty ) RelStr ) ) ;

cluster inf_net N : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over R : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( non empty strict directed ) ( non empty strict directed ) prenet of R : ( ( non empty ) ( non empty ) RelStr ) ) -> non empty transitive strict directed ;

end;

registration

let R be ( ( non empty ) ( non empty ) RelStr ) ;
let N be ( ( non empty transitive directed ) ( non empty transitive directed ) net of R : ( ( non empty ) ( non empty ) RelStr ) ) ;

cluster inf_net N : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over R : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( non empty strict directed ) ( non empty transitive strict directed ) prenet of R : ( ( non empty ) ( non empty ) RelStr ) ) -> non empty strict directed ;

end;

registration

let R be ( ( non empty reflexive antisymmetric /\-complete ) ( non empty reflexive antisymmetric with_infima lower-bounded /\-complete ) RelStr ) ;
let N be ( ( non empty transitive directed ) ( non empty transitive directed ) net of R : ( ( non empty reflexive antisymmetric /\-complete ) ( non empty reflexive antisymmetric with_infima lower-bounded /\-complete ) RelStr ) ) ;

cluster inf_net N : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over R : ( ( non empty reflexive antisymmetric /\-complete ) ( non empty reflexive antisymmetric with_infima lower-bounded /\-complete ) RelStr ) ) : ( ( non empty strict directed ) ( non empty transitive strict directed ) prenet of R : ( ( non empty reflexive antisymmetric /\-complete ) ( non empty reflexive antisymmetric with_infima lower-bounded /\-complete ) RelStr ) ) -> non empty strict directed monotone ;

end;

registration

let R be ( ( non empty reflexive antisymmetric /\-complete ) ( non empty reflexive antisymmetric with_infima lower-bounded /\-complete ) RelStr ) ;
let N be ( ( non empty transitive directed ) ( non empty transitive directed ) net of R : ( ( non empty reflexive antisymmetric /\-complete ) ( non empty reflexive antisymmetric with_infima lower-bounded /\-complete ) RelStr ) ) ;

cluster inf_net N : ( ( non empty transitive directed ) ( non empty transitive directed ) NetStr over R : ( ( non empty reflexive antisymmetric /\-complete ) ( non empty reflexive antisymmetric with_infima lower-bounded /\-complete ) RelStr ) ) : ( ( non empty strict directed ) ( non empty transitive strict directed monotone eventually-directed ) prenet of R : ( ( non empty reflexive antisymmetric /\-complete ) ( non empty reflexive antisymmetric with_infima lower-bounded /\-complete ) RelStr ) ) -> non empty strict directed eventually-directed ;

end;

theorem :: WAYBEL32:23

for R being ( ( non empty ) ( non empty ) RelStr )
for N being ( ( non empty transitive directed ) ( non empty transitive directed ) net of R : ( ( non empty ) ( non empty ) RelStr ) ) holds rng the mapping of (inf_net N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) RelStr ) ) ) : ( ( non empty strict directed ) ( non empty transitive strict directed ) prenet of b₁ : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( Function-like V18( the carrier of (inf_net b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) RelStr ) ) ) : ( ( non empty strict directed ) ( non empty transitive strict directed ) prenet of b₁ : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( non empty Relation-like the carrier of (inf_net b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) RelStr ) ) ) : ( ( non empty strict directed ) ( non empty transitive strict directed ) prenet of b₁ : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( ) ( non empty ) set ) -defined the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18( the carrier of (inf_net b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) RelStr ) ) ) : ( ( non empty strict directed ) ( non empty transitive strict directed ) prenet of b₁ : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Element of bool [: the carrier of (inf_net b₂ : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) RelStr ) ) ) : ( ( non empty strict directed ) ( non empty transitive strict directed ) prenet of b₁ : ( ( non empty ) ( non empty ) RelStr ) ) : ( ( ) ( non empty ) set ) , the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) Element of bool the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = { ("/\" ( { (N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty ) ( non empty ) RelStr ) ) . i : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) where i is ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : i : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) >= j : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) } ,R : ( ( non empty ) ( non empty ) RelStr ) )) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) where j is ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : verum } ;

theorem :: WAYBEL32:24

for R being ( ( reflexive transitive antisymmetric with_suprema with_infima up-complete /\-complete ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() up-complete /\-complete ) LATTICE)
for N being ( ( non empty transitive directed ) ( non empty transitive directed ) net of R : ( ( reflexive transitive antisymmetric with_suprema with_infima up-complete /\-complete ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() up-complete /\-complete ) LATTICE) ) holds sup (inf_net N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima up-complete /\-complete ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() up-complete /\-complete ) LATTICE) ) ) : ( ( non empty strict directed ) ( non empty transitive strict directed monotone eventually-directed ) prenet of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima up-complete /\-complete ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() up-complete /\-complete ) LATTICE) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima up-complete /\-complete ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() up-complete /\-complete ) LATTICE) : ( ( ) ( non empty ) set ) ) = lim_inf N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima up-complete /\-complete ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() up-complete /\-complete ) LATTICE) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima up-complete /\-complete ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() up-complete /\-complete ) LATTICE) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL32:25

for R being ( ( reflexive transitive antisymmetric with_suprema with_infima up-complete /\-complete ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() up-complete /\-complete ) LATTICE)
for N being ( ( non empty transitive directed ) ( non empty transitive directed ) net of R : ( ( reflexive transitive antisymmetric with_suprema with_infima up-complete /\-complete ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() up-complete /\-complete ) LATTICE) )
for i being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds sup (inf_net N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima up-complete /\-complete ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() up-complete /\-complete ) LATTICE) ) ) : ( ( non empty strict directed ) ( non empty transitive strict directed monotone eventually-directed ) prenet of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima up-complete /\-complete ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() up-complete /\-complete ) LATTICE) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima up-complete /\-complete ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() up-complete /\-complete ) LATTICE) : ( ( ) ( non empty ) set ) ) = lim_inf (N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima up-complete /\-complete ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() up-complete /\-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 up-complete /\-complete ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() up-complete /\-complete ) LATTICE) ) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( reflexive transitive antisymmetric with_suprema with_infima up-complete /\-complete ) ( non empty reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() up-complete /\-complete ) LATTICE) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL32:26

for R being ( ( reflexive transitive antisymmetric with_infima /\-complete ) ( non empty reflexive transitive antisymmetric with_infima lower-bounded /\-complete ) Semilattice)
for N being ( ( non empty transitive directed ) ( non empty transitive directed ) net of R : ( ( reflexive transitive antisymmetric with_infima /\-complete ) ( non empty reflexive transitive antisymmetric with_infima lower-bounded /\-complete ) Semilattice) )
for V being ( ( upper ) ( upper ) Subset of ) st inf_net N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( reflexive transitive antisymmetric with_infima /\-complete ) ( non empty reflexive transitive antisymmetric with_infima lower-bounded /\-complete ) Semilattice) ) : ( ( non empty strict directed ) ( non empty transitive strict directed monotone eventually-directed ) prenet of b₁ : ( ( reflexive transitive antisymmetric with_infima /\-complete ) ( non empty reflexive transitive antisymmetric with_infima lower-bounded /\-complete ) Semilattice) ) is_eventually_in V : ( ( upper ) ( upper ) Subset of ) holds
N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( reflexive transitive antisymmetric with_infima /\-complete ) ( non empty reflexive transitive antisymmetric with_infima lower-bounded /\-complete ) Semilattice) ) is_eventually_in V : ( ( upper ) ( upper ) Subset of ) ;

theorem :: WAYBEL32:27

for R being ( ( reflexive transitive antisymmetric with_infima /\-complete ) ( non empty reflexive transitive antisymmetric with_infima lower-bounded /\-complete ) Semilattice)
for N being ( ( non empty transitive directed ) ( non empty transitive directed ) net of R : ( ( reflexive transitive antisymmetric with_infima /\-complete ) ( non empty reflexive transitive antisymmetric with_infima lower-bounded /\-complete ) Semilattice) )
for V being ( ( lower ) ( lower ) Subset of ) st N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( reflexive transitive antisymmetric with_infima /\-complete ) ( non empty reflexive transitive antisymmetric with_infima lower-bounded /\-complete ) Semilattice) ) is_eventually_in V : ( ( lower ) ( lower ) Subset of ) holds
inf_net N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( reflexive transitive antisymmetric with_infima /\-complete ) ( non empty reflexive transitive antisymmetric with_infima lower-bounded /\-complete ) Semilattice) ) : ( ( non empty strict directed ) ( non empty transitive strict directed monotone eventually-directed ) prenet of b₁ : ( ( reflexive transitive antisymmetric with_infima /\-complete ) ( non empty reflexive transitive antisymmetric with_infima lower-bounded /\-complete ) Semilattice) ) is_eventually_in V : ( ( lower ) ( lower ) Subset of ) ;

theorem :: WAYBEL32:28

for R being ( ( non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima up-complete /\-complete order_consistent ) ( non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() up-complete /\-complete order_consistent ) TopLattice)
for N being ( ( non empty transitive directed ) ( non empty transitive directed ) net of R : ( ( non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima up-complete /\-complete order_consistent ) ( non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() up-complete /\-complete order_consistent ) TopLattice) )
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= lim_inf N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima up-complete /\-complete order_consistent ) ( non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() up-complete /\-complete order_consistent ) TopLattice) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima up-complete /\-complete order_consistent ) ( non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() up-complete /\-complete order_consistent ) TopLattice) : ( ( ) ( non empty ) set ) ) holds
x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is_a_cluster_point_of N : ( ( non empty transitive directed ) ( non empty transitive directed ) net of b₁ : ( ( non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima up-complete /\-complete order_consistent ) ( non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() up-complete /\-complete order_consistent ) TopLattice) ) ;

theorem :: WAYBEL32:29

for R being ( ( non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima up-complete /\-complete order_consistent ) ( non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() up-complete /\-complete order_consistent ) TopLattice)
for N being ( ( non empty transitive directed eventually-directed ) ( non empty transitive directed eventually-directed ) net of R : ( ( non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima up-complete /\-complete order_consistent ) ( non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() up-complete /\-complete order_consistent ) TopLattice) )
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= lim_inf N : ( ( non empty transitive directed eventually-directed ) ( non empty transitive directed eventually-directed ) net of b₁ : ( ( non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima up-complete /\-complete order_consistent ) ( non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() up-complete /\-complete order_consistent ) TopLattice) ) : ( ( ) ( ) Element of the carrier of b₁ : ( ( non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima up-complete /\-complete order_consistent ) ( non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() up-complete /\-complete order_consistent ) TopLattice) : ( ( ) ( non empty ) set ) ) iff x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is_a_cluster_point_of N : ( ( non empty transitive directed eventually-directed ) ( non empty transitive directed eventually-directed ) net of b₁ : ( ( non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima up-complete /\-complete order_consistent ) ( non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V126() up-complete /\-complete order_consistent ) TopLattice) ) ) ;