A3: R is_reflexive_in field R by Def9;
A4: P is_reflexive_in field P by Def9;

now :: thesis: for a being set st a in field (P \/ R) holds
[a,a] in P \/ R

let a be set ; :: thesis: ( a in field (P \/ R) implies [a,a] in P \/ R )

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

assume a in field P ; :: thesis: [a,a] in P \/ R
then [a,a] in P by A4, Def1;
hence [a,a] in P \/ R by XBOOLE_0:def 3; :: thesis: verum

end;

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

assume a in field R ; :: thesis: [a,a] in P \/ R
then [a,a] in R by A3, Def1;
hence [a,a] in P \/ R by XBOOLE_0:def 3; :: thesis: verum

end;

assume a in field (P \/ R) ; :: thesis: [a,a] in P \/ R
then a in (field P) \/ (field R) by RELAT_1:18;
hence [a,a] in P \/ R by A5, A6, XBOOLE_0:def 3; :: thesis: verum

end;

hence P \/ R is reflexive by Def1, Def9; :: thesis: verum