for TS being TopSpace
for P being Subset of TS st P is closed holds
( P is boundary iff for Q being Subset of TS st Q <> {} & Q is open holds
ex G being Subset of TS st
( G c= Q & G <> {} & G is open & P misses G ) )