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

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