let T be non empty reflexive transitive antisymmetric up-complete Scott TopRelStr ; :: thesis: T is T_0-TopSpace
reconsider T' = T as Scott TopAugmentation of T by YELLOW_9:44;

now

let x, y be Point of T'; :: thesis: ( x <> y implies Cl {x} <> Cl {y} )
reconsider x' = x, y' = y as Element of T' ;
A1: ( Cl {x'} = downarrow x' & Cl {y'} = downarrow y' ) by Th9;
assume x <> y ; :: thesis: Cl {x} <> Cl {y}
hence Cl {x} <> Cl {y} by A1, WAYBEL_0:19; :: thesis: verum

end;

hence T is T_0-TopSpace by TSP_1:def 5; :: thesis: verum