let S be complete Scott TopLattice; :: thesis: S is monotone-convergence
let D be non empty directed Subset of (Omega S); :: according to WAYBEL25:def 4 :: thesis: ( ex_sup_of D, Omega S & ( for V being open Subset of S st sup D in V holds
D meets V ) )
thus ex_sup_of D, Omega S by YELLOW_0:17; :: thesis: for V being open Subset of S st sup D in V holds
D meets V
A1: Omega S = TopRelStr(# the carrier of S, the InternalRel of S, the topology of S #) by Th15;
then A2: RelStr(# the carrier of (Omega S), the InternalRel of (Omega S) #) = RelStr(# the carrier of S, the InternalRel of S #) ;
reconsider E = D as Subset of S by A1;
let V be open Subset of S; :: thesis: ( sup D in V implies D meets V )
assume sup D in V ; :: thesis: D meets V
then A3: sup E in V by A2, YELLOW_0:17, YELLOW_0:26;
E is non empty directed Subset of S by A2, WAYBEL_0:3;
hence D meets V by A3, WAYBEL11:def 1; :: thesis: verum