let S be up-complete /\-complete Semilattice; :: thesis: for T being Scott TopAugmentation of S holds sigma S = the topology of T
let T be Scott TopAugmentation of S; :: thesis: sigma S = the topology of T
thus sigma S c= the topology of T :: according to XBOOLE_0:def 10 :: thesis: the topology of T c= sigma S

proof

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in sigma S or e in the topology of T )
assume A1: e in sigma S ; :: thesis: e in the topology of T
then reconsider A = e as Subset of S ;
A2: RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of T,the InternalRel of T #) by YELLOW_9:def 4;
then reconsider A' = A as Subset of T ;
( A is inaccessible_by_directed_joins & A is upper ) by A1, Th14;
then ( A' is inaccessible_by_directed_joins & A' is upper ) by A2, WAYBEL_0:25, YELLOW_9:47;
then A' is open ;
hence e in the topology of T by PRE_TOPC:def 5; :: thesis: verum

end;

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in the topology of T or e in sigma S )
assume A3: e in the topology of T ; :: thesis: e in sigma S
then reconsider A = e as Subset of T ;
A is open by A3, PRE_TOPC:def 5;
then A4: ( A is inaccessible_by_directed_joins & A is upper ) ;
A5: RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of T,the InternalRel of T #) by YELLOW_9:def 4;
then reconsider A' = A as Subset of S ;
A' is inaccessible_by_directed_joins

proof

let D be non empty directed Subset of S; :: according to WAYBEL11:def 1 :: thesis: ( not "\/" D,S in A' or not D misses A' )
assume A6: sup D in A' ; :: thesis: not D misses A'
reconsider E = D as Subset of T by A5;
ex a being Element of S st
( a is_>=_than D & ( for b being Element of S st b is_>=_than D holds
a <= b ) ) by WAYBEL_0:def 39;
then ex_sup_of D,S by YELLOW_0:15;
then ( E is directed & sup D = sup E ) by A5, WAYBEL_0:3, YELLOW_0:26;
hence not D misses A' by A4, A6, WAYBEL11:def 1; :: thesis: verum

end;

then ( A' is inaccessible_by_directed_joins & A' is upper ) by A4, A5, WAYBEL_0:25;
hence e in sigma S by Th14; :: thesis: verum