A1:
R is_reflexive_in field R
by Def9;

A2: P is_reflexive_in field P by Def9;

A2: P is_reflexive_in field P by Def9;

now :: thesis: for a being object st a in field (P \/ R) holds

[a,a] in P \/ R

hence
P \/ R is reflexive
by Def1; :: thesis: verum[a,a] in P \/ R

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

then a in (field P) \/ (field R) by RELAT_1:18;

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

end;A3: 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 A2;

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

end;then [a,a] in P by A2;

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

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

assume
a in field (P \/ R)
; :: thesis: [a,a] in P \/ Rassume
a in field R
; :: thesis: [a,a] in P \/ R

then [a,a] in R by A1;

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

end;then [a,a] in R by A1;

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

then a in (field P) \/ (field R) by RELAT_1:18;

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