:: deftheorem defines <-> MSAFREE5:def 30 :
for x, y being object holds x <-> y = {[x,y],[y,x]};