let S be complete Scott TopLattice; :: thesis: for T being correct Lawson TopAugmentation of S
for A being Subset of S st A is open holds
for C being Subset of T st C = A holds
C is open
let T be correct Lawson TopAugmentation of S; :: thesis: for A being Subset of S st A is open holds
for C being Subset of T st C = A holds
C is open
let A be Subset of S; :: thesis: ( A is open implies for C being Subset of T st C = A holds
C is open )
assume A1: A in the topology of S ; :: according to PRE_TOPC:def 2 :: thesis: for C being Subset of T st C = A holds
C is open
let C be Subset of T; :: thesis: ( C = A implies C is open )
assume A2: C = A ; :: thesis: C is open
(sigma T) \/ (omega T) is prebasis of T by Def3;
then A3: (sigma T) \/ (omega T) c= the topology of T by TOPS_2:64;
RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of T, the InternalRel of T #) by YELLOW_9:def 4;
then S is Scott TopAugmentation of T by YELLOW_9:def 4;
then A in sigma T by A1, YELLOW_9:51;
then C in (sigma T) \/ (omega T) by A2, XBOOLE_0:def 3;
hence C in the topology of T by A3; :: according to PRE_TOPC:def 2 :: thesis: verum