:: deftheorem defines trivial SUBSET_1:def 7 :
for X being set holds
( X is trivial iff for x, y being Element of X holds x = y );