let T be injective T_0-TopSpace; :: thesis: ( T is compact & T is locally-compact & T is sober )
consider S being Scott TopAugmentation of Omega T;
A1: TopStruct(# the carrier of S,the topology of S #) = TopStruct(# the carrier of T,the topology of T #) by Th37;
( S is compact & S is locally-compact & S is sober ) by WAYBEL14:32;
hence ( T is compact & T is locally-compact & T is sober ) by A1, YELLOW14:27, YELLOW14:28, YELLOW14:29; :: thesis: verum