:: deftheorem defines proper SUBSET_1:def 6 :
for E being set
for A being Subset of E holds
( A is proper iff A <> E );