let X be non empty TopSpace; :: thesis: for A being Subset of X st A is boundary holds
A <> the carrier of X
let A be Subset of X; :: thesis: ( A is boundary implies A <> the carrier of X )
assume A1: Int A = {} ; :: according to TOPS_3:def 1 :: thesis: A <> the carrier of X
assume A = the carrier of X ; :: thesis: contradiction
then A = [#] X ;
hence contradiction by A1, TOPS_1:15; :: thesis: verum