A15:
R is_symmetric_in field R
by Def11;

A16: P is_symmetric_in field P by Def11;

A16: P is_symmetric_in field P by Def11;

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

[b,a] in P \ R

hence
P \ R is symmetric
by Def3; :: thesis: verum[b,a] in P \ R

let a, b be object ; :: 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

A17: [a,b] in P \ R ; :: thesis: [b,a] in P \ R

not [a,b] in R by A17, XBOOLE_0:def 5;

then A18: ( not b in field R or not a in field R or not [b,a] in R ) by A15;

A19: [a,b] in P by A17, XBOOLE_0:def 5;

then ( a in field P & b in field P ) by RELAT_1:15;

then A20: [b,a] in P by A16, A19;

( ( 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 A20, A18, XBOOLE_0:def 5; :: thesis: verum

end;assume that

a in field (P \ R) and

b in field (P \ R) and

A17: [a,b] in P \ R ; :: thesis: [b,a] in P \ R

not [a,b] in R by A17, XBOOLE_0:def 5;

then A18: ( not b in field R or not a in field R or not [b,a] in R ) by A15;

A19: [a,b] in P by A17, XBOOLE_0:def 5;

then ( a in field P & b in field P ) by RELAT_1:15;

then A20: [b,a] in P by A16, A19;

( ( 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 A20, A18, XBOOLE_0:def 5; :: thesis: verum