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

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 )

hence
not A is maximal_anti-discrete
; :: thesis: verum( 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;thus ( C is anti-discrete & A c= C & A <> C ) by Th6; :: thesis: verum