let T be injective T_0-TopSpace; :: thesis: T is monotone-convergence
set S = the Scott TopAugmentation of Omega T;
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 monotone-convergence by Th27; :: thesis: verum