let T be continuous complete TopLattice; :: thesis: ( T is Scott implies ( T is injective & T is T_0 ) )
assume T is Scott ; :: thesis: ( T is injective & T is T_0 )
then T is Scott TopAugmentation of T by YELLOW_9:44;
hence ( T is injective & T is T_0 ) ; :: thesis: verum