let X be non empty TopSpace; :: thesis: for A being Subset of X st A is anti-discrete & not A is open holds
A is boundary
let A be Subset of X; :: thesis: ( A is anti-discrete & not A is open implies A is boundary )
A1: Int A c= A by TOPS_1:16;
assume A is anti-discrete ; :: thesis: ( A is open or A is boundary )
then ( A misses Int A or A c= Int A ) ;
then A2: ( A /\ (Int A) = {} or A c= Int A ) ;
assume A3: not A is open ; :: thesis: A is boundary
assume not A is boundary ; :: thesis: contradiction
then Int A <> {} by TOPS_1:48;
hence contradiction by A3, A2, A1, XBOOLE_0:def 10, XBOOLE_1:28; :: thesis: verum