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

now

let a be set ; :: thesis: ( a in field (P \/ R) implies [a,a] in P \/ R )
assume a in field (P \/ R) ; :: thesis: [a,a] in P \/ R
then A5: a in (field P) \/ (field R) by RELAT_1:33;

A6: now

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

end;

now

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

end;

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

end;

then P \/ R is_reflexive_in field (P \/ R) by Def1;
hence P \/ R is reflexive by Def9; :: thesis: P /\ R is reflexive

now

let a be set ; :: thesis: ( a in field (P /\ R) implies [a,a] in P /\ R )
A7: field (P /\ R) c= (field P) /\ (field R) by RELAT_1:34;
assume a in field (P /\ R) ; :: thesis: [a,a] in P /\ R
then ( a in field P & a in field R ) by A7, XBOOLE_0:def 4;
then ( [a,a] in P & [a,a] in R ) by A3, A4, Def1;
hence [a,a] in P /\ R by XBOOLE_0:def 4; :: thesis: verum

end;

then P /\ R is_reflexive_in field (P /\ R) by Def1;
hence P /\ R is reflexive by Def9; :: thesis: verum