let X be non empty TopSpace; :: thesis: for A0 being non empty Subset of X st A0 is T_0 holds

ex X0 being strict Kolmogorov_subspace of X st A0 = the carrier of X0

let A0 be non empty Subset of X; :: thesis: ( A0 is T_0 implies ex X0 being strict Kolmogorov_subspace of X st A0 = the carrier of X0 )

consider X0 being non empty strict SubSpace of X such that

A1: A0 = the carrier of X0 by TSEP_1:10;

assume A0 is T_0 ; :: thesis: ex X0 being strict Kolmogorov_subspace of X st A0 = the carrier of X0

then reconsider X0 = X0 as strict Kolmogorov_subspace of X by A1, Th13;

take X0 ; :: thesis: A0 = the carrier of X0

thus A0 = the carrier of X0 by A1; :: thesis: verum

ex X0 being strict Kolmogorov_subspace of X st A0 = the carrier of X0

let A0 be non empty Subset of X; :: thesis: ( A0 is T_0 implies ex X0 being strict Kolmogorov_subspace of X st A0 = the carrier of X0 )

consider X0 being non empty strict SubSpace of X such that

A1: A0 = the carrier of X0 by TSEP_1:10;

assume A0 is T_0 ; :: thesis: ex X0 being strict Kolmogorov_subspace of X st A0 = the carrier of X0

then reconsider X0 = X0 as strict Kolmogorov_subspace of X by A1, Th13;

take X0 ; :: thesis: A0 = the carrier of X0

thus A0 = the carrier of X0 by A1; :: thesis: verum