for X being non empty TopSpace ex M being Subset of X st M is maximal_T_0