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