:: deftheorem Def1 defines proper TEX_2:def 1 :
for Y being TopStruct
for IT being SubSpace of Y holds
( IT is proper iff for A being Subset of Y st A = the carrier of IT holds
A is proper );