let X be non empty TopSpace; :: thesis: for A being Subset of X st ( A is open or A is closed ) & A is maximal_T_0 holds
not A is proper
let A be Subset of X; :: thesis: ( ( A is open or A is closed ) & A is maximal_T_0 implies not A is proper )
assume ( A is open or A is closed ) ; :: thesis: ( not A is maximal_T_0 or not A is proper )
then A1: A = MaxADSet A by TEX_4:58, TEX_4:62;
assume A is maximal_T_0 ; :: thesis: not A is proper
then A = the carrier of X by A1, Def5;
hence not A is proper by SUBSET_1:def 7; :: thesis: verum