theorem :: TOPS_1:50

for TS being TopSpace
for P being Subset of TS holds
( P is boundary iff for Q being Subset of TS st Q c= P & Q is open holds
Q = {} )