let a, b be object ; :: thesis: for R being Relation st R = {[a,b]} holds
R ~ = {[b,a]}
let R be Relation; :: thesis: ( R = {[a,b]} implies R ~ = {[b,a]} )
assume R = {[a,b]} ; :: thesis: R ~ = {[b,a]}
then ( dom R = {a} & rng R = {b} ) by RELAT_1:9;
then ( dom (R ~) = {b} & rng (R ~) = {a} ) by RELAT_1:20;
hence R ~ = {[b,a]} by RELAT_1:189; :: thesis: verum