:: deftheorem defines c= TARSKI:def 3 :
for X, Y being set holds
( X c= Y iff for x being object st x in X holds
x in Y );