let L be non empty up-complete Poset; :: thesis: for S1, S2 being Scott TopAugmentation of L holds the topology of S1 = the topology of S2
let S1, S2 be Scott TopAugmentation of L; :: thesis: the topology of S1 = the topology of S2
A1: RelStr(# the carrier of S1, the InternalRel of S1 #) = RelStr(# the carrier of L, the InternalRel of L #) by YELLOW_9:def 4
.= RelStr(# the carrier of S2, the InternalRel of S2 #) by YELLOW_9:def 4 ;
thus the topology of S1 c= the topology of S2 :: according to XBOOLE_0:def 10 :: thesis: the topology of S2 c= the topology of S1

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the topology of S1 or x in the topology of S2 )
assume x in the topology of S1 ; :: thesis: x in the topology of S2
then reconsider y = x as open Subset of S1 by PRE_TOPC:def 2;
reconsider z = y as Subset of S2 by A1;
( z is inaccessible & z is upper ) by A1, WAYBEL_0:25, YELLOW_9:47;
hence x in the topology of S2 by PRE_TOPC:def 2; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the topology of S2 or x in the topology of S1 )
assume x in the topology of S2 ; :: thesis: x in the topology of S1
then reconsider y = x as open Subset of S2 by PRE_TOPC:def 2;
reconsider z = y as Subset of S1 by A1;
( z is inaccessible & z is upper ) by A1, WAYBEL_0:25, YELLOW_9:47;
hence x in the topology of S1 by PRE_TOPC:def 2; :: thesis: verum