consider x being Element of r;
consider y, z being set such that
A1: x = [y,z] by RELAT_1:def 1;
[z,y] in r ~ by A1, RELAT_1:def 7;
hence r ~ is non empty Relation of B,A ; :: thesis: verum