let T be complete Scott TopLattice; :: thesis: T is T_0-TopSpace

now :: thesis: for x, y being Point of T st x <> y holds
Cl {x} <> Cl {y}

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

end;

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