let R be complete LATTICE; :: 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 Def4;
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 ) ) by A1, WAYBEL11:31, A2, Th47, WAYBEL_0:25; :: thesis: ( not S is inaccessible_by_directed_joins or not S is upper or S is open )
assume ( S is inaccessible & S is upper ) ; :: thesis: S is open
then ( A is inaccessible & A is upper ) by A2, Th47, WAYBEL_0:25;
hence S in the topology of T by A1, WAYBEL11:31; :: according to PRE_TOPC:def 2 :: thesis: verum

end;

hence T is Scott ; :: thesis: verum