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
A15: [a,b] in P \ R ; :: thesis: [b,a] in P \ R
not [a,b] in R by A15, XBOOLE_0:def 5;
then A16: ( not b in field R or not a in field R or not [b,a] in R ) by A3, Def3;
A17: [a,b] in P by A15, XBOOLE_0:def 5;
then ( a in field P & b in field P ) by RELAT_1:15;
then A18: [b,a] in P by A4, A17, Def3;
( ( not b in field R or not a in field R ) implies not [b,a] in R ) by RELAT_1:15;
hence [b,a] in P \ R by A18, A16, XBOOLE_0:def 5; :: thesis: verum

end;

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