let Y be non empty TopStruct ; :: thesis: for A being empty Subset of Y holds not A is maximal_anti-discrete
consider a being set such that
A1: a in the carrier of Y by XBOOLE_0:def 1;
reconsider a = a as Point of Y by A1;
let A be empty Subset of Y; :: thesis: not A is maximal_anti-discrete

now

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

end;

hence not A is maximal_anti-discrete by Def7; :: thesis: verum