let X be non empty TopSpace; :: thesis: for A being empty Subset of X holds not A is maximal_discrete
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_discrete

now :: thesis: ex C being Element of bool the carrier of X st
( C is discrete & A c= C & A <> C )

take C = {a}; :: thesis: ( C is discrete & A c= C & A <> C )
thus ( C is discrete & A c= C & A <> C ) by Th30, XBOOLE_1:2; :: thesis: verum

end;

hence not A is maximal_discrete ; :: thesis: verum