:: deftheorem DIFF defines -different MSAFREE5:def 3 :
for a, b being object holds
( b is a -different iff b <> a );