A7:
R is_symmetric_in field R
by Def11;

A8: P is_symmetric_in field P by Def11;

A8: 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

A9: ( a in field (P /\ R) & b in field (P /\ R) ) and

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

A11: [a,b] in R by A10, XBOOLE_0:def 4;

A12: field (P /\ R) c= (field P) /\ (field R) by RELAT_1:19;

then ( a in field R & b in field R ) by A9, XBOOLE_0:def 4;

then A13: [b,a] in R by A7, A11;

A14: [a,b] in P by A10, XBOOLE_0:def 4;

( a in field P & b in field P ) by A12, A9, XBOOLE_0:def 4;

then [b,a] in P by A8, A14;

hence [b,a] in P /\ R by A13, XBOOLE_0:def 4; :: thesis: verum

end;assume that

A9: ( a in field (P /\ R) & b in field (P /\ R) ) and

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

A11: [a,b] in R by A10, XBOOLE_0:def 4;

A12: field (P /\ R) c= (field P) /\ (field R) by RELAT_1:19;

then ( a in field R & b in field R ) by A9, XBOOLE_0:def 4;

then A13: [b,a] in R by A7, A11;

A14: [a,b] in P by A10, XBOOLE_0:def 4;

( a in field P & b in field P ) by A12, A9, XBOOLE_0:def 4;

then [b,a] in P by A8, A14;

hence [b,a] in P /\ R by A13, XBOOLE_0:def 4; :: thesis: verum