let X be non-Kolmogorov_space; :: thesis: for A0 being Subset of X st not A0 is T_0 holds
ex X0 being strict non-Kolmogorov_subspace of X st A0 = the carrier of X0
let A0 be Subset of X; :: thesis: ( not A0 is T_0 implies ex X0 being strict non-Kolmogorov_subspace of X st A0 = the carrier of X0 )
assume A1: not A0 is T_0 ; :: thesis: ex X0 being strict non-Kolmogorov_subspace of X st A0 = the carrier of X0
then not A0 is empty ;
then consider X0 being non empty strict SubSpace of X such that
A2: A0 = the carrier of X0 by TSEP_1:10;
reconsider X0 = X0 as strict T_0 SubSpace of X by A1, A2, Th13;
take X0 ; :: thesis: A0 = the carrier of X0
thus A0 = the carrier of X0 by A2; :: thesis: verum