let R be up-complete /\-complete Semilattice; :: thesis: for T being TopAugmentation of R st the topology of T = sigma R holds
T is Scott
let T be TopAugmentation of R; :: thesis: ( the topology of T = sigma R implies T is Scott )
assume A1: the topology of T = sigma R ; :: thesis: T is Scott
A2: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of R, the InternalRel of R #) by YELLOW_9:def 4;
T is Scott

proof

let S be Subset of T; :: according to WAYBEL11:def 4 :: thesis: ( ( not S is open or ( S is inaccessible_by_directed_joins & S is upper ) ) & ( not S is inaccessible_by_directed_joins or not S is upper or S is open ) )
reconsider A = S as Subset of R by A2;
thus ( S is open implies ( S is inaccessible & S is upper ) ) :: thesis: ( not S is inaccessible_by_directed_joins or not S is upper or S is open )

proof

assume S is open ; :: thesis: ( S is inaccessible & S is upper )
then S in the topology of T by PRE_TOPC:def 2;
then ( A is inaccessible & A is upper ) by A1, Th10;
hence ( S is inaccessible & S is upper ) by A2, WAYBEL_0:25, YELLOW_9:47; :: thesis: verum

end;

assume A3: ( S is inaccessible & S is upper ) ; :: thesis: S is open
A is inaccessible

proof

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

end;

then ( A is inaccessible & A is upper ) by A2, A3, WAYBEL_0:25;
then A in the topology of T by A1, Th10;
hence S is open by PRE_TOPC:def 2; :: thesis: verum

end;

hence T is Scott ; :: thesis: verum