:: deftheorem defines = XBOOLE_0:def 10 :
for X, Y being set holds
( X = Y iff ( X c= Y & Y c= X ) );