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 by Def5;
then A2: Cl (MaxADSet M) = MaxADSet M by PRE_TOPC:52;
MaxADSet M = the carrier of X by A1, Def5;
then Cl M = the carrier of X by A2, TEX_4:64;
hence M is dense by TOPS_3:def 2; :: thesis: verum