defpred S₁[ set , set ] means [$2,$1] in R;
consider P being Relation such that
A1: for x, y being set holds
( [x,y] in P iff ( x in rng R & y in dom R & S₁[x,y] ) ) from RELAT_1:sch 1();
take P ; :: thesis: for x, y being set holds
( [x,y] in P iff [y,x] in R )
let x, y be set ; :: thesis: ( [x,y] in P iff [y,x] in R )
( [y,x] in R implies ( y in dom R & x in rng R ) ) by Def4, Def5;
hence ( [x,y] in P iff [y,x] in R ) by A1; :: thesis: verum