let R be non empty reflexive RelStr ; for T being TopAugmentation of R st the topology of T = sigma R holds
T is correct
let T be TopAugmentation of R; ( the topology of T = sigma R implies T is correct )
assume A1:
the topology of T = sigma R
; 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; verum