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 A1: 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
let V be open Subset of S; :: thesis: ( sup D in V implies D meets V )
assume A2: sup D in V ; :: thesis: D meets V
A3: Omega S = TopRelStr(# the carrier of S,the InternalRel of S,the topology of S #) by Th15;
then A4: 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 A3;
A5: E is non empty directed Subset of S by A4, WAYBEL_0:3;
sup E in V by A1, A2, A4, YELLOW_0:26;
hence D meets V by A5, WAYBEL11:def 1; :: thesis: verum