let X be non empty TopSpace; :: thesis: for A being empty Subset of X holds not A is maximal_T_0
consider a being object such that
A1: a in the carrier of X by XBOOLE_0:def 1;
reconsider a = a as Point of X by A1;
let A be empty Subset of X; :: thesis: not A is maximal_T_0
now :: thesis: ex C being Element of bool the carrier of X st
( C is T_0 & A c= C & A <> C )
take C = {a}; :: thesis: ( C is T_0 & A c= C & A <> C )
thus ( C is T_0 & A c= C & A <> C ) by TSP_1:12, XBOOLE_1:2; :: thesis: verum
end;
hence not A is maximal_T_0 ; :: thesis: verum