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

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