:: deftheorem Def1 defines boundary TOPS_3:def 1 :
for X being TopStruct
for A being Subset of X holds
( A is boundary iff Int A = {} );