let P, R be Relation; :: thesis: ( P is symmetric & R is symmetric implies ( P \/ R is symmetric & P /\ R is symmetric & P \ R is symmetric ) )
assume that
A1: P is symmetric and
A2: R is symmetric ; :: thesis: ( P \/ R is symmetric & P /\ R is symmetric & P \ R is symmetric )
A3: R is_symmetric_in field R by A2, Def11;
A4: P is_symmetric_in field P by A1, Def11;

now

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

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

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;

then P \/ R is_symmetric_in field (P \/ R) by Def3;
hence P \/ R is symmetric by Def11; :: thesis: ( P /\ R is symmetric & P \ R is symmetric )

now

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
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 A3, A11, Def3;
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 A4, A14, Def3;
hence [b,a] in P /\ R by A13, XBOOLE_0:def 4; :: thesis: verum

end;

then P /\ R is_symmetric_in field (P /\ R) by Def3;
hence P /\ R is symmetric by Def11; :: thesis: P \ R is symmetric

now

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;

then P \ R is_symmetric_in field (P \ R) by Def3;
hence P \ R is symmetric by Def11; :: thesis: verum