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:29;
then consider M being Subset of X such that
{} X c= M and
A1: M is maximal_T_0 by Th9, TSP_1:9;
take M ; :: thesis: M is maximal_T_0
thus M is maximal_T_0 by A1; :: thesis: verum