let S be complete LATTICE; :: thesis: for T being Scott TopAugmentation of S holds the topology of T = sigma S
let T be Scott TopAugmentation of S; :: thesis: the topology of T = sigma S
set R = TopRelStr(# the carrier of S,the InternalRel of S,(sigma S) #);
RelStr(# the carrier of TopRelStr(# the carrier of S,the InternalRel of S,(sigma S) #),the InternalRel of TopRelStr(# the carrier of S,the InternalRel of S,(sigma S) #) #) = RelStr(# the carrier of S,the InternalRel of S #) ;
then reconsider R = TopRelStr(# the carrier of S,the InternalRel of S,(sigma S) #) as TopAugmentation of S by Def4;
reconsider R = R as correct Scott TopAugmentation of S by Th48, Th49;
A1: RelStr(# the carrier of T,the InternalRel of T #) = RelStr(# the carrier of R,the InternalRel of R #) by Def4;
thus the topology of T c= sigma S :: according to XBOOLE_0:def 10 :: thesis: sigma S c= the topology of T

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the topology of T or x in sigma S )
assume A2: x in the topology of T ; :: thesis: x in sigma S
then reconsider A = x as Subset of T ;
reconsider C = A as Subset of R by A1;
A is open by A2, PRE_TOPC:def 5;
then C is open by A1, Th50;
hence x in sigma S by PRE_TOPC:def 5; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in sigma S or x in the topology of T )
assume A3: x in sigma S ; :: thesis: x in the topology of T
then reconsider A = x as Subset of R ;
reconsider C = A as Subset of T by A1;
A is open by A3, PRE_TOPC:def 5;
then C is open by A1, Th50;
hence x in the topology of T by PRE_TOPC:def 5; :: thesis: verum