let X be TopSpace; :: thesis: for A being Subset of X holds
( A is boundary iff for G being Subset of X st G <> {} & G is open holds
A ` meets G )
let A be Subset of X; :: thesis: ( A is boundary iff for G being Subset of X st G <> {} & G is open holds
A ` meets G )
thus ( A is boundary implies for G being Subset of X st G <> {} & G is open holds
A ` meets G ) by SUBSET_1:24, TOPS_1:50; :: thesis: ( ( for G being Subset of X st G <> {} & G is open holds
A ` meets G ) implies A is boundary )
assume A1: for G being Subset of X st G <> {} & G is open holds
A ` meets G ; :: thesis: A is boundary
assume Int A <> {} ; :: according to TOPS_3:def 1 :: thesis: contradiction
then ( Int A c= A & A ` meets Int A ) by A1, TOPS_1:16;
hence contradiction by SUBSET_1:24; :: thesis: verum