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

now

let a be set ; :: thesis: ( a in field (P \/ R) implies not [a,a] in P \/ R )
assume a in field (P \/ R) ; :: thesis: not [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: not [a,a] in P \/ R
then A7: not [a,a] in P by A3, Def2;
A8: ( a in field R implies not [a,a] in R ) by A4, Def2;
( not a in field R implies not [a,a] in R ) by RELAT_1:30;
hence not [a,a] in P \/ R by A7, A8, XBOOLE_0:def 3; :: thesis: verum

end;

now

assume a in field R ; :: thesis: not [a,a] in P \/ R
then A9: not [a,a] in R by A4, Def2;
A10: ( a in field P implies not [a,a] in P ) by A3, Def2;
( not a in field P implies not [a,a] in P ) by RELAT_1:30;
hence not [a,a] in P \/ R by A9, A10, XBOOLE_0:def 3; :: thesis: verum

end;

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

end;

then P \/ R is_irreflexive_in field (P \/ R) by Def2;
hence P \/ R is irreflexive by Def10; :: thesis: P /\ R is irreflexive

now

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

end;

then P /\ R is_irreflexive_in field (P /\ R) by Def2;
hence P /\ R is irreflexive by Def10; :: thesis: verum