theorem LemS: :: MSAFREE5:95

for a, b being object holds
( dom (a <-> b) = {a,b} & (a <-> b) . a = b & (a <-> b) . b = a & rng (a <-> b) = {a,b} )