:: deftheorem defines without_proper_subsets ARMSTRNG:def 27 :
for X being set holds
( X is without_proper_subsets iff for x, y being set st x in X & y in X & x c= y holds
x = y );