theorem :: TOPS_3:13

for X being TopSpace
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 )