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 object ; :: 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 A9 = A as Subset of T ;
( A is inaccessible & A is upper ) by A1, Th10;
then ( A9 is inaccessible & A9 is upper ) by A2, WAYBEL_0:25, YELLOW_9:47;
hence e in the topology of T by PRE_TOPC:def 2; :: thesis: verum

end;

let e be object ; :: 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 ;
A4: A is open by A3, PRE_TOPC:def 2;
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 A9 = A as Subset of S ;
A9 is inaccessible

proof

let D be non empty directed Subset of S; :: according to WAYBEL11:def 1 :: thesis: ( not "\/" (D,S) in A9 or not D misses A9 )
assume A6: sup D in A9 ; :: thesis: not D misses A9
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 A7: ex_sup_of D,S by YELLOW_0:15;
A8: E is directed by A5, WAYBEL_0:3;
sup D = sup E by A5, A7, YELLOW_0:26;
hence not D misses A9 by A4, A6, A8, WAYBEL11:def 1; :: thesis: verum

end;

then ( A9 is inaccessible & A9 is upper ) by A4, A5, WAYBEL_0:25;
hence e in sigma S by Th10; :: thesis: verum