let X be non empty TopSpace; :: thesis: ex M being Subset of X st M is maximal_T_0
set A = {} X;
{} X is discrete by TEX_2:35;
then {} X is T_0 by TSP_1:11;
then consider M being Subset of X such that
{} X c= M and
A1: M is maximal_T_0 by Th9;
take M ; :: thesis: M is maximal_T_0
thus M is maximal_T_0 by A1; :: thesis: verum