let a, b be object ; :: thesis: ( dom (a <-> b) = {a,b} & (a <-> b) . a = b & (a <-> b) . b = a & rng (a <-> b) = {a,b} )
( [a,b] in a <-> b & [b,a] in a <-> b ) by TARSKI:def 2;
hence ( dom (a <-> b) = {a,b} & (a <-> b) . a = b & (a <-> b) . b = a & rng (a <-> b) = {a,b} ) by RELAT_1:10, FUNCT_1:1; :: thesis: verum