let Y be non empty TopStruct ; :: thesis: for A being empty Subset of Y holds not A is maximal_anti-discrete
consider a being object 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 :: thesis: ex C being Element of bool the carrier of Y st
( C is anti-discrete & A c= C & A <> C )

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

end;

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