A5:
R is_reflexive_in field R
by Def9;

A6: P is_reflexive_in field P by Def9;

A6: 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 )

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

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

then a in field R by A7, XBOOLE_0:def 4;

then A9: [a,a] in R by A5;

a in field P by A8, A7, XBOOLE_0:def 4;

then [a,a] in P by A6;

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

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

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

then a in field R by A7, XBOOLE_0:def 4;

then A9: [a,a] in R by A5;

a in field P by A8, A7, XBOOLE_0:def 4;

then [a,a] in P by A6;

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