:: deftheorem Def5 defines ~ RELAT_1:def 7 :
for R, b₂ being Relation holds
( b₂ = R ~ iff for x, y being object holds
( [x,y] in b₂ iff [y,x] in R ) );