defpred S1[ object , object ] means [$2,$1] in R;
consider P being Relation such that
A1:
for x, y being object holds
( [x,y] in P iff ( x in rng R & y in dom R & S1[x,y] ) )
from RELAT_1:sch 1();
take
P
; for x, y being object holds
( [x,y] in P iff [y,x] in R )
let x, y be object ; ( [x,y] in P iff [y,x] in R )
( [y,x] in R implies ( y in dom R & x in rng R ) )
by XTUPLE_0:def 12, XTUPLE_0:def 13;
hence
( [x,y] in P iff [y,x] in R )
by A1; verum