A1:
R is_symmetric_in field R
by Def11;

A2: P is_symmetric_in field P by Def11;

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

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

end;assume that

a in field (P \/ R) and

b in field (P \/ R) and

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

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

assume A5:
[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 A1, A5;

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

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

then [b,a] in R by A1, A5;

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

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

hence
[b,a] in P \/ R
by A3, A4, XBOOLE_0:def 3; :: thesis: verumassume A6:
[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 A2, A6;

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

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

then [b,a] in P by A2, A6;

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