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 )

A5: now

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

end;

A8: now

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

end;

assume a in field (P \/ R) ; :: thesis: not [a,a] in P \/ R
then a in (field P) \/ (field R) by RELAT_1:18;
hence not [a,a] in P \/ R by A5, A8, 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 )
assume A11: a in field (P /\ R) ; :: thesis: not [a,a] in P /\ R
field (P /\ R) c= (field P) /\ (field R) by RELAT_1:19;
then a in field P by A11, XBOOLE_0:def 4;
then not [a,a] in P by A3, 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