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

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

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 S2 or x in the topology of S1 )
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;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

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