A3: R is_symmetric_in field R by Def11;
A4: P is_symmetric_in field P by Def11;

now :: thesis: for a, b being set st a in field (P \/ R) & b in field (P \/ R) & [a,b] in P \/ R holds
[b,a] in P \/ R

let a, b be set ; :: thesis: ( a in field (P \/ R) & b in field (P \/ R) & [a,b] in P \/ R implies [b,a] in P \/ R )
assume that
a in field (P \/ R) and
b in field (P \/ R) and
A5: [a,b] in P \/ R ; :: thesis: [b,a] in P \/ R

A6: now :: thesis: ( [a,b] in R implies [b,a] in P \/ R )

assume A7: [a,b] in R ; :: thesis: [b,a] in P \/ R
then ( a in field R & b in field R ) by RELAT_1:15;
then [b,a] in R by A3, A7, Def3;
hence [b,a] in P \/ R by XBOOLE_0:def 3; :: thesis: verum

end;

now :: thesis: ( [a,b] in P implies [b,a] in P \/ R )

assume A8: [a,b] in P ; :: thesis: [b,a] in P \/ R
then ( a in field P & b in field P ) by RELAT_1:15;
then [b,a] in P by A4, A8, Def3;
hence [b,a] in P \/ R by XBOOLE_0:def 3; :: thesis: verum

end;

hence [b,a] in P \/ R by A5, A6, XBOOLE_0:def 3; :: thesis: verum

end;

hence P \/ R is symmetric by Def3, Def11; :: thesis: verum