:: WAYBEL14 semantic presentation

begin

theorem :: WAYBEL14:1
for X being ( ( ) ( ) set )
for F being ( ( finite ) ( finite ) Subset-Family of ) ex G being ( ( finite ) ( finite ) Subset-Family of ) st
( G : ( ( finite ) ( finite ) Subset-Family of ) c= F : ( ( finite ) ( finite ) Subset-Family of ) & union G : ( ( finite ) ( finite ) Subset-Family of ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = union F : ( ( finite ) ( finite ) Subset-Family of ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) & ( for g being ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) st g : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) in G : ( ( finite ) ( finite ) Subset-Family of ) holds
not g : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) c= union (G : ( ( finite ) ( finite ) Subset-Family of ) \ {g : ( ( ) ( ) Subset of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non empty trivial finite 1 : ( ( ) ( non empty V11() V12() V13() V17() V18() finite cardinal ) Element of K46() : ( ( ) ( non empty non trivial V11() V12() V13() non finite cardinal limit_cardinal ) Element of bool K42() : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) -element ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( finite ) Element of bool (bool b1 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool b1 : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: WAYBEL14:2
for S being ( ( ) ( ) 1-sorted )
for X being ( ( ) ( ) Subset of ) holds
( X : ( ( ) ( ) Subset of ) ` : ( ( ) ( ) Element of bool the carrier of b1 : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = the carrier of S : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) iff X : ( ( ) ( ) Subset of ) is empty ) ;

theorem :: WAYBEL14:3
for R being ( ( non empty transitive antisymmetric with_infima ) ( non empty transitive antisymmetric with_infima ) RelStr )
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds downarrow (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\" y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty transitive antisymmetric with_infima ) ( non empty transitive antisymmetric with_infima ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( lower ) Element of bool the carrier of b1 : ( ( non empty transitive antisymmetric with_infima ) ( non empty transitive antisymmetric with_infima ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = (downarrow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( lower ) Element of bool the carrier of b1 : ( ( non empty transitive antisymmetric with_infima ) ( non empty transitive antisymmetric with_infima ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) /\ (downarrow y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( lower ) Element of bool the carrier of b1 : ( ( non empty transitive antisymmetric with_infima ) ( non empty transitive antisymmetric with_infima ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( non empty transitive antisymmetric with_infima ) ( non empty transitive antisymmetric with_infima ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL14:4
for R being ( ( non empty transitive antisymmetric with_suprema ) ( non empty transitive antisymmetric with_suprema ) RelStr )
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds uparrow (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "\/" y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty transitive antisymmetric with_suprema ) ( non empty transitive antisymmetric with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( upper ) Element of bool the carrier of b1 : ( ( non empty transitive antisymmetric with_suprema ) ( non empty transitive antisymmetric with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = (uparrow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( upper ) Element of bool the carrier of b1 : ( ( non empty transitive antisymmetric with_suprema ) ( non empty transitive antisymmetric with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) /\ (uparrow y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( upper ) Element of bool the carrier of b1 : ( ( non empty transitive antisymmetric with_suprema ) ( non empty transitive antisymmetric with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( non empty transitive antisymmetric with_suprema ) ( non empty transitive antisymmetric with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL14:5
for L being ( ( non empty antisymmetric complete ) ( non empty antisymmetric lower-bounded upper-bounded V112() with_suprema with_infima complete ) RelStr )
for X being ( ( lower ) ( lower ) Subset of ) st sup X : ( ( lower ) ( lower ) Subset of ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty antisymmetric complete ) ( non empty antisymmetric lower-bounded upper-bounded V112() with_suprema with_infima complete ) RelStr ) : ( ( ) ( non empty ) set ) ) in X : ( ( lower ) ( lower ) Subset of ) holds
X : ( ( lower ) ( lower ) Subset of ) = downarrow (sup X : ( ( lower ) ( lower ) Subset of ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty antisymmetric complete ) ( non empty antisymmetric lower-bounded upper-bounded V112() with_suprema with_infima complete ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( non empty antisymmetric complete ) ( non empty antisymmetric lower-bounded upper-bounded V112() with_suprema with_infima complete ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL14:6
for L being ( ( non empty antisymmetric complete ) ( non empty antisymmetric lower-bounded upper-bounded V112() with_suprema with_infima complete ) RelStr )
for X being ( ( upper ) ( upper ) Subset of ) st inf X : ( ( upper ) ( upper ) Subset of ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty antisymmetric complete ) ( non empty antisymmetric lower-bounded upper-bounded V112() with_suprema with_infima complete ) RelStr ) : ( ( ) ( non empty ) set ) ) in X : ( ( upper ) ( upper ) Subset of ) holds
X : ( ( upper ) ( upper ) Subset of ) = uparrow (inf X : ( ( upper ) ( upper ) Subset of ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty antisymmetric complete ) ( non empty antisymmetric lower-bounded upper-bounded V112() with_suprema with_infima complete ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( non empty antisymmetric complete ) ( non empty antisymmetric lower-bounded upper-bounded V112() with_suprema with_infima complete ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL14:7
for R being ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr )
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) << y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) iff uparrow y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty filtered upper ) Element of bool the carrier of b1 : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) c= wayabove x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( upper ) Element of bool the carrier of b1 : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: WAYBEL14:8
for R being ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr )
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) << y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) iff downarrow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty directed lower ) Element of bool the carrier of b1 : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) c= waybelow y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( lower ) Element of bool the carrier of b1 : ( ( non empty reflexive transitive ) ( non empty reflexive transitive ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: WAYBEL14:9
for R being ( ( non empty reflexive antisymmetric complete ) ( non empty reflexive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete ) RelStr )
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( sup (waybelow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) Element of bool the carrier of b1 : ( ( non empty reflexive antisymmetric complete ) ( non empty reflexive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty reflexive antisymmetric complete ) ( non empty reflexive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete ) RelStr ) : ( ( ) ( non empty ) set ) ) <= x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= inf (wayabove x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( non empty reflexive antisymmetric complete ) ( non empty reflexive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty reflexive antisymmetric complete ) ( non empty reflexive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ;

theorem :: WAYBEL14:10
for L being ( ( non empty antisymmetric lower-bounded ) ( non empty antisymmetric lower-bounded ) RelStr ) holds uparrow (Bottom L : ( ( non empty antisymmetric lower-bounded ) ( non empty antisymmetric lower-bounded ) RelStr ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty antisymmetric lower-bounded ) ( non empty antisymmetric lower-bounded ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( non empty antisymmetric lower-bounded ) ( non empty antisymmetric lower-bounded ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = the carrier of L : ( ( non empty antisymmetric lower-bounded ) ( non empty antisymmetric lower-bounded ) RelStr ) : ( ( ) ( non empty ) set ) ;

theorem :: WAYBEL14:11
for L being ( ( non empty antisymmetric upper-bounded ) ( non empty antisymmetric upper-bounded ) RelStr ) holds downarrow (Top L : ( ( non empty antisymmetric upper-bounded ) ( non empty antisymmetric upper-bounded ) RelStr ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty antisymmetric upper-bounded ) ( non empty antisymmetric upper-bounded ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( non empty antisymmetric upper-bounded ) ( non empty antisymmetric upper-bounded ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = the carrier of L : ( ( non empty antisymmetric upper-bounded ) ( non empty antisymmetric upper-bounded ) RelStr ) : ( ( ) ( non empty ) set ) ;

theorem :: WAYBEL14:12
for P being ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) Poset)
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds (wayabove x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( upper ) Element of bool the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) Poset) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) "\/" (wayabove y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( upper ) Element of bool the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) Poset) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( upper ) Element of bool the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) Poset) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) c= uparrow (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "\/" y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) Poset) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty filtered upper ) Element of bool the carrier of b1 : ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) Poset) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL14:13
for P being ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima ) Poset)
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds (waybelow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( lower ) Element of bool the carrier of b1 : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima ) Poset) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) "/\" (waybelow y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( lower ) Element of bool the carrier of b1 : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima ) Poset) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima ) Poset) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) c= downarrow (x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\" y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima ) Poset) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty directed lower ) Element of bool the carrier of b1 : ( ( reflexive transitive antisymmetric with_infima ) ( non empty reflexive transitive antisymmetric with_infima ) Poset) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL14:14
for R being ( ( non empty reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) Poset)
for l being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( l : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is co-prime iff for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( not l : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "\/" y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) Poset) : ( ( ) ( non empty ) set ) ) or l : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) or l : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: WAYBEL14:15
for P being ( ( non empty reflexive transitive antisymmetric complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete ) Poset)
for V being ( ( non empty ) ( non empty ) Subset of ) holds downarrow (inf V : ( ( non empty ) ( non empty ) Subset of ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty reflexive transitive antisymmetric complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete ) Poset) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty directed lower ) Element of bool the carrier of b1 : ( ( non empty reflexive transitive antisymmetric complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete ) Poset) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = meet { (downarrow u : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty directed lower ) Element of bool the carrier of b1 : ( ( non empty reflexive transitive antisymmetric complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete ) Poset) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) where u is ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : u : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in V : ( ( non empty ) ( non empty ) Subset of ) } : ( ( ) ( ) set ) ;

theorem :: WAYBEL14:16
for P being ( ( non empty reflexive transitive antisymmetric complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete ) Poset)
for V being ( ( non empty ) ( non empty ) Subset of ) holds uparrow (sup V : ( ( non empty ) ( non empty ) Subset of ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty reflexive transitive antisymmetric complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete ) Poset) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty filtered upper ) Element of bool the carrier of b1 : ( ( non empty reflexive transitive antisymmetric complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete ) Poset) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = meet { (uparrow u : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty filtered upper ) Element of bool the carrier of b1 : ( ( non empty reflexive transitive antisymmetric complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete ) Poset) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) where u is ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : u : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in V : ( ( non empty ) ( non empty ) Subset of ) } : ( ( ) ( ) set ) ;

registration
let L be ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) sup-Semilattice) ;
let x be ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;
cluster compactbelow x : ( ( ) ( ) Element of the carrier of L : ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of bool the carrier of L : ( ( reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -> directed ;
end;

theorem :: WAYBEL14:17
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for S being ( ( irreducible ) ( non empty irreducible ) Subset of )
for V being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) st V : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) = S : ( ( irreducible ) ( non empty irreducible ) Subset of ) ` : ( ( ) ( ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) holds
V : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) is prime ;

theorem :: WAYBEL14:18
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) "\/" y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( ) Element of the carrier of (InclPoset the topology of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Element of bool (bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete ) RelStr ) : ( ( ) ( non empty non trivial ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) \/ y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( ) set ) & x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) "/\" y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( ) Element of the carrier of (InclPoset the topology of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Element of bool (bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete ) RelStr ) : ( ( ) ( non empty non trivial ) set ) ) = x : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) /\ y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: WAYBEL14:19
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for V being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
( V : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) is prime iff for X, Y being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
( not X : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) /\ Y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( ) set ) c= V : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) or X : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) c= V : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) or Y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) c= V : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ) ) ;

theorem :: WAYBEL14:20
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for V being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
( V : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) is co-prime iff for X, Y being ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) holds
( not V : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) c= X : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) \/ Y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) : ( ( ) ( ) set ) or V : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) c= X : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) or V : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) c= Y : ( ( ) ( ) Element of ( ( ) ( non empty non trivial ) set ) ) ) ) ;

registration
let T be ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ;
cluster InclPoset the topology of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) Element of bool (bool the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete ) RelStr ) -> strict distributive ;
end;

theorem :: WAYBEL14:21
for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace)
for L being ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima ) ( non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima ) TopLattice)
for t being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for l being ( ( ) ( ) Point of ( ( ) ( non empty ) set ) )
for X being ( ( ) ( ) Subset-Family of ) st TopStruct(# the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the topology of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Element of bool (bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict TopSpace-like ) TopStruct ) = TopStruct(# the carrier of L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima ) ( non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima ) TopLattice) : ( ( ) ( non empty ) set ) , the topology of L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima ) ( non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima ) TopLattice) : ( ( ) ( non empty ) Element of bool (bool the carrier of b2 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima ) ( non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima ) TopLattice) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict TopSpace-like ) TopStruct ) & t : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) = l : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) & X : ( ( ) ( ) Subset-Family of ) is ( ( open b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) -quasi_basis ) ( open b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) -quasi_basis ) Basis of l : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) holds
X : ( ( ) ( ) Subset-Family of ) is ( ( open b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) -quasi_basis ) ( open b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) -quasi_basis ) Basis of t : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ;

theorem :: WAYBEL14:22
for L being ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima ) ( non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima ) TopLattice)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st ( for X being ( ( ) ( ) Subset of ) st X : ( ( ) ( ) Subset of ) is open holds
X : ( ( ) ( ) Subset of ) is upper ) holds
uparrow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty filtered upper ) Element of bool the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima ) ( non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima ) TopLattice) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is compact ;

begin

registration
let L be ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete ) LATTICE) ;
cluster sigma L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete ) RelStr ) : ( ( ) ( ) Element of bool (bool the carrier of L : ( ( reflexive transitive antisymmetric with_suprema with_infima complete ) ( non empty reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -> non empty ;
end;

theorem :: WAYBEL14:23
for L being ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) holds sigma L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) Element of bool (bool the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) = the topology of L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) Element of bool (bool the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL14:24
for L being ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice)
for X being ( ( ) ( ) Subset of ) holds
( X : ( ( ) ( ) Subset of ) in sigma L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) Element of bool (bool the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) iff X : ( ( ) ( ) Subset of ) is open ) ;

theorem :: WAYBEL14:25
for L being ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice)
for VV being ( ( ) ( ) Subset of )
for X being ( ( filtered ) ( filtered ) Subset of ) st VV : ( ( ) ( ) Subset of ) = { ((downarrow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty directed lower property(S) ) Element of bool the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) `) : ( ( ) ( upper closed_under_directed_sups ) Element of bool the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) where x is ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in X : ( ( filtered ) ( filtered ) Subset of ) } holds
VV : ( ( ) ( ) Subset of ) is directed ;

theorem :: WAYBEL14:26
for L being ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for X being ( ( ) ( ) Subset of ) st X : ( ( ) ( ) Subset of ) is open & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in X : ( ( ) ( ) Subset of ) holds
inf X : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) ) << x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

definition
let R be ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ;
let f be ( ( Function-like V36( the carrier of [:R : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ,R : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) :] : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) , the carrier of R : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) ) ( V22() V25( the carrier of [:R : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ,R : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) :] : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) ) V26( the carrier of R : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) Function-like V36( the carrier of [:R : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) ,R : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) :] : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) , the carrier of R : ( ( non empty reflexive ) ( non empty reflexive ) RelStr ) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( ) set ) , ( ( ) ( non empty ) set ) ) ;
attr f is jointly_Scott-continuous means :: WAYBEL14:def 1
 for T being ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) st TopStruct(# the carrier of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) , the topology of T : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) Element of bool (bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) #) : ( ( strict ) ( non empty strict TopSpace-like ) TopStruct ) = ConvergenceSpace (Scott-Convergence R : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( ) ( V22() ) Convergence-Class of R : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) ) : ( ( strict ) ( strict ) TopStruct ) holds
ex ft being ( ( Function-like V36( the carrier of [:b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) ( V22() V25( the carrier of [:b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) Function-like V36( the carrier of [:b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) st
( ft : ( ( Function-like V36( the carrier of [:b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) ( V22() V25( the carrier of [:b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) Function-like V36( the carrier of [:b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) = f : ( ( ) ( ) Element of the carrier of R : ( ( TopSpace-like ) ( TopSpace-like ) TopStruct ) : ( ( ) ( ) set ) ) & ft : ( ( Function-like V36( the carrier of [:b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) ( V22() V25( the carrier of [:b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) ) V26( the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) Function-like V36( the carrier of [:b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) ,b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) :] : ( ( strict TopSpace-like ) ( non empty strict TopSpace-like ) TopStruct ) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) ) ) Function of ( ( ) ( non empty ) set ) , ( ( ) ( non empty ) set ) ) is continuous );
end;

theorem :: WAYBEL14:27
for L being ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice)
for X being ( ( ) ( ) Subset of )
for V being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st V : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = X : ( ( ) ( ) Subset of ) holds
( V : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is co-prime iff ( X : ( ( ) ( ) Subset of ) is filtered & X : ( ( ) ( ) Subset of ) is upper ) ) ;

theorem :: WAYBEL14:28
for L being ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice)
for X being ( ( ) ( ) Subset of )
for V being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st V : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = X : ( ( ) ( ) Subset of ) & ex x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st X : ( ( ) ( ) Subset of ) = (downarrow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty directed lower property(S) ) Element of bool the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ` : ( ( ) ( upper closed_under_directed_sups ) Element of bool the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) holds
( V : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is prime & V : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> the carrier of L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL14:29
for L being ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice)
for X being ( ( ) ( ) Subset of )
for V being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st V : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = X : ( ( ) ( ) Subset of ) & sup_op L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( Function-like V36( the carrier of [:b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ,b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) :] : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) ) ) ( V22() V25( the carrier of [:b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ,b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) :] : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) ) V26( the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) ) Function-like V36( the carrier of [:b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ,b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) :] : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) ) ) Element of bool [: the carrier of [:b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ,b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) :] : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) is jointly_Scott-continuous & V : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is prime & V : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> the carrier of L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) holds
ex x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st X : ( ( ) ( ) Subset of ) = (downarrow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty directed lower property(S) ) Element of bool the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ` : ( ( ) ( upper closed_under_directed_sups ) Element of bool the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL14:30
for L being ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) st L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) is continuous holds
sup_op L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( Function-like V36( the carrier of [:b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ,b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) :] : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) ) ) ( V22() V25( the carrier of [:b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ,b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) :] : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) ) V26( the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) ) Function-like V36( the carrier of [:b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ,b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) :] : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) ) ) Element of bool [: the carrier of [:b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ,b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) :] : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) is jointly_Scott-continuous ;

theorem :: WAYBEL14:31
for L being ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) st sup_op L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( Function-like V36( the carrier of [:b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ,b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) :] : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) ) ) ( V22() V25( the carrier of [:b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ,b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) :] : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) ) V26( the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) ) Function-like V36( the carrier of [:b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ,b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) :] : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) ) ) Element of bool [: the carrier of [:b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ,b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) :] : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) is jointly_Scott-continuous holds
L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) is sober ;

theorem :: WAYBEL14:32
for L being ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) st L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) is continuous holds
( L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) is compact & L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) is locally-compact & L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) is sober & L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) is Baire ) ;

theorem :: WAYBEL14:33
for L being ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice)
for X being ( ( ) ( ) Subset of ) st L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) is continuous & X : ( ( ) ( ) Subset of ) in sigma L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) Element of bool (bool the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) holds
X : ( ( ) ( ) Subset of ) = union { (wayabove x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( upper ) Element of bool the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) where x is ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in X : ( ( ) ( ) Subset of ) } : ( ( ) ( ) set ) ;

theorem :: WAYBEL14:34
for L being ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) st ( for X being ( ( ) ( ) Subset of ) st X : ( ( ) ( ) Subset of ) in sigma L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) Element of bool (bool the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) holds
X : ( ( ) ( ) Subset of ) = union { (wayabove x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( upper ) Element of bool the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) where x is ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in X : ( ( ) ( ) Subset of ) } : ( ( ) ( ) set ) ) holds
L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) is continuous ;

theorem :: WAYBEL14:35
for L being ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) is continuous holds
ex B being ( ( open b2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) -quasi_basis ) ( open b2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) -quasi_basis ) Basis of x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) st
for X being ( ( ) ( ) Subset of ) st X : ( ( ) ( ) Subset of ) in B : ( ( open b2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) -quasi_basis ) ( open b2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) -quasi_basis ) Basis of b2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) holds
( X : ( ( ) ( ) Subset of ) is open & X : ( ( ) ( ) Subset of ) is filtered ) ;

theorem :: WAYBEL14:36
for L being ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) st L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) is continuous holds
InclPoset (sigma L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric ) RelStr ) is continuous ;

theorem :: WAYBEL14:37
for L being ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice)
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st ( for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ex B being ( ( open b3 : ( ( ) ( ) Subset of ) -quasi_basis ) ( open b3 : ( ( ) ( ) Subset of ) -quasi_basis ) Basis of x : ( ( ) ( ) Subset of ) ) st
for Y being ( ( ) ( ) Subset of ) st Y : ( ( ) ( ) Subset of ) in B : ( ( open b3 : ( ( ) ( ) Subset of ) -quasi_basis ) ( open b3 : ( ( ) ( ) Subset of ) -quasi_basis ) Basis of b3 : ( ( ) ( ) Subset of ) ) holds
( Y : ( ( ) ( ) Subset of ) is open & Y : ( ( ) ( ) Subset of ) is filtered ) ) & InclPoset (sigma L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric ) RelStr ) is continuous holds
x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = "\/" ( { (inf X : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) ) where X is ( ( ) ( ) Subset of ) : ( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in X : ( ( ) ( ) Subset of ) & X : ( ( ) ( ) Subset of ) in sigma L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) Element of bool (bool the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) } ,L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) ) ;

theorem :: WAYBEL14:38
for L being ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) st ( for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = "\/" ( { (inf X : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) ) where X is ( ( ) ( ) Subset of ) : ( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in X : ( ( ) ( ) Subset of ) & X : ( ( ) ( ) Subset of ) in sigma L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) Element of bool (bool the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) } ,L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) ) ) holds
L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) is continuous ;

theorem :: WAYBEL14:39
for L being ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) holds
( ( for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ex B being ( ( open b2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) -quasi_basis ) ( open b2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) -quasi_basis ) Basis of x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) st
for Y being ( ( ) ( ) Subset of ) st Y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in B : ( ( ) ( ) Subset of ) holds
( Y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is open & Y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is filtered ) ) iff for V being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ex VV being ( ( ) ( ) Subset of ) st
( V : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = sup VV : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of the carrier of (InclPoset (sigma b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) ) & ( for W being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st W : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in VV : ( ( ) ( ) Subset of ) holds
W : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is co-prime ) ) ) ;

theorem :: WAYBEL14:40
for L being ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) holds
( ( ( for V being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ex VV being ( ( ) ( ) Subset of ) st
( V : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = sup VV : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of the carrier of (InclPoset (sigma b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) ) & ( for W being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st W : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in VV : ( ( ) ( ) Subset of ) holds
W : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is co-prime ) ) ) & InclPoset (sigma L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric ) RelStr ) is continuous ) iff InclPoset (sigma L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric ) RelStr ) is completely-distributive ) ;

theorem :: WAYBEL14:41
for L being ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) holds
( InclPoset (sigma L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric ) RelStr ) is completely-distributive iff ( InclPoset (sigma L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric ) RelStr ) is continuous & (InclPoset (sigma L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric ) RelStr ) opp : ( ( strict ) ( non empty strict reflexive transitive antisymmetric ) RelStr ) is continuous ) ) ;

theorem :: WAYBEL14:42
for L being ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) st L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) is algebraic holds
ex B being ( ( open V99(b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) ) ( open V99(b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) ) Basis of L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) st B : ( ( open V99(b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) ) ( open V99(b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) ) Basis of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) = { (uparrow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty filtered upper ) Element of bool the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) where x is ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in the carrier of (CompactSublatt L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) : ( ( strict V113(b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) ) ( non empty strict reflexive transitive antisymmetric V113(b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) join-inheriting with_suprema ) SubRelStr of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) : ( ( ) ( non empty ) set ) } ;

theorem :: WAYBEL14:43
for L being ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) st ex B being ( ( open V99(b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) ) ( open V99(b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) ) Basis of L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) st B : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = { (uparrow x : ( ( ) ( ) Subset of ) ) : ( ( ) ( ) Element of bool the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) where x is ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : x : ( ( ) ( ) Subset of ) in the carrier of (CompactSublatt L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) : ( ( strict V113(b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) ) ( non empty strict reflexive transitive antisymmetric V113(b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) join-inheriting with_suprema ) SubRelStr of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) : ( ( ) ( non empty ) set ) } holds
( InclPoset (sigma L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric ) RelStr ) is algebraic & ( for V being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ex VV being ( ( ) ( ) Subset of ) st
( V : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = sup VV : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of the carrier of (InclPoset (sigma b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) ) & ( for W being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st W : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in VV : ( ( ) ( ) Subset of ) holds
W : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is co-prime ) ) ) ) ;

theorem :: WAYBEL14:44
for L being ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) st InclPoset (sigma L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric ) RelStr ) is algebraic & ( for V being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ex VV being ( ( ) ( ) Subset of ) st
( V : ( ( open V99(b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) ) ( open V99(b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) ) Basis of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) = sup VV : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (InclPoset (sigma b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) : ( ( ) ( non empty ) Element of bool (bool the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty strict reflexive transitive antisymmetric ) RelStr ) : ( ( ) ( non empty ) set ) ) & ( for W being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st W : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in VV : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
W : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is co-prime ) ) ) holds
ex B being ( ( open V99(b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) ) ( open V99(b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) ) Basis of L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) st B : ( ( open V99(b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) ) ( open V99(b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) ) Basis of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) = { (uparrow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty filtered upper ) Element of bool the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) where x is ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in the carrier of (CompactSublatt L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) : ( ( strict V113(b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) ) ( non empty strict reflexive transitive antisymmetric V113(b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) join-inheriting with_suprema ) SubRelStr of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) : ( ( ) ( non empty ) set ) } ;

theorem :: WAYBEL14:45
for L being ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) st ex B being ( ( open V99(b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) ) ( open V99(b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) ) Basis of L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) st B : ( ( open V99(b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) ) ( open V99(b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) ) Basis of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) = { (uparrow x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty filtered upper ) Element of bool the carrier of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) where x is ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in the carrier of (CompactSublatt L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) : ( ( strict V113(b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) ) ( non empty strict reflexive transitive antisymmetric V113(b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) join-inheriting with_suprema ) SubRelStr of b1 : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) ) : ( ( ) ( non empty ) set ) } holds
L : ( ( TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete Scott ) ( non empty TopSpace-like reflexive transitive antisymmetric lower-bounded upper-bounded V112() up-complete /\-complete with_suprema with_infima complete Scott ) TopLattice) is algebraic ;