theorem Lemma7: :: PREFER_1:9

for a, b being object
for R being Relation st R = {[a,b]} holds
R ~ = {[b,a]}