set x = the Element of r;
consider y, z being set such that
A1: the Element of r = [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