let X be non empty almost_discrete TopSpace; :: thesis: for A being Subset of X st ( A is open or A is closed ) & A is maximal_discrete holds
not A is proper
let A be Subset of X; :: thesis: ( ( A is open or A is closed ) & A is maximal_discrete implies not A is proper )
assume A1: ( A is open or A is closed ) ; :: thesis: ( not A is maximal_discrete or not A is proper )
then A is closed by TDLAT_3:21;
then A2: A = Cl A by PRE_TOPC:22;
assume A3: A is maximal_discrete ; :: thesis: not A is proper
A is open by A1, TDLAT_3:22;
then A is dense by A3, Th41;
then A = the carrier of X by A2, TOPS_3:def 2;
hence not A is proper ; :: thesis: verum