let X be non empty TopSpace; :: thesis: for M being Subset of X st M is maximal_T_0 holds
M is dense
let M be Subset of X; :: thesis: ( M is maximal_T_0 implies M is dense )
assume A1: M is maximal_T_0 ; :: thesis: M is dense
then MaxADSet M = [#] X ;
then A2: Cl (MaxADSet M) = MaxADSet M by PRE_TOPC:22;
MaxADSet M = the carrier of X by A1;
then Cl M = the carrier of X by A2, TEX_4:62;
hence M is dense by TOPS_3:def 2; :: thesis: verum