let Y be non empty TopStruct ; :: thesis: for A being non empty Subset of Y st A is anti-discrete & A is closed holds

A is maximal_anti-discrete

let A be non empty Subset of Y; :: thesis: ( A is anti-discrete & A is closed implies A is maximal_anti-discrete )

assume A1: A is anti-discrete ; :: thesis: ( not A is closed or A is maximal_anti-discrete )

assume A2: A is closed ; :: thesis: A is maximal_anti-discrete

for D being Subset of Y st D is anti-discrete & A c= D holds

A = D

A is maximal_anti-discrete

let A be non empty Subset of Y; :: thesis: ( A is anti-discrete & A is closed implies A is maximal_anti-discrete )

assume A1: A is anti-discrete ; :: thesis: ( not A is closed or A is maximal_anti-discrete )

assume A2: A is closed ; :: thesis: A is maximal_anti-discrete

for D being Subset of Y st D is anti-discrete & A c= D holds

A = D

proof

hence
A is maximal_anti-discrete
by A1; :: thesis: verum
let D be Subset of Y; :: thesis: ( D is anti-discrete & A c= D implies A = D )

assume D is anti-discrete ; :: thesis: ( not A c= D or A = D )

then ( D misses A or D c= A ) by A2;

then A3: ( D /\ A = {} or D c= A ) ;

assume A c= D ; :: thesis: A = D

hence A = D by A3, XBOOLE_1:28; :: thesis: verum

end;assume D is anti-discrete ; :: thesis: ( not A c= D or A = D )

then ( D misses A or D c= A ) by A2;

then A3: ( D /\ A = {} or D c= A ) ;

assume A c= D ; :: thesis: A = D

hence A = D by A3, XBOOLE_1:28; :: thesis: verum