let R be non empty reflexive RelStr ; :: thesis: for T being TopAugmentation of R st the topology of T = sigma R holds
T is correct
let T be TopAugmentation of R; :: thesis: ( the topology of T = sigma R implies T is correct )
assume A1: the topology of T = sigma R ; :: thesis: T is correct
A2: RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of R, the InternalRel of R #) by Def4;
set IT = ConvergenceSpace (Scott-Convergence R);
A3: the carrier of (ConvergenceSpace (Scott-Convergence R)) = the carrier of R by YELLOW_6:def 24;
then A4: the carrier of T in sigma R by A2, PRE_TOPC:def 1;
A5: for a being Subset-Family of T st a c= the topology of T holds
union a in the topology of T by A1, A2, A3, PRE_TOPC:def 1;
for a, b being Subset of T st a in the topology of T & b in the topology of T holds
a /\ b in the topology of T by A1, PRE_TOPC:def 1;
hence T is correct by A1, A4, A5; :: thesis: verum