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 )
assume A1: A is anti-discrete ; :: thesis: ( A is open or A is boundary )
assume A2: not A is open ; :: thesis: A is boundary
assume not A is boundary ; :: thesis: contradiction
then A3: Int A <> {} by TOPS_1:84;
( A misses Int A or A c= Int A ) by A1, Def3;
then A4: ( A /\ (Int A) = {} or A c= Int A ) by XBOOLE_0:def 7;
Int A c= A by TOPS_1:44;
hence contradiction by A2, A3, A4, XBOOLE_0:def 10, XBOOLE_1:28; :: thesis: verum