A1: P is_irreflexive_in field P by Def10;
A2: R is_irreflexive_in field R by Def10;
let a be object ; :: according to RELAT_2:def 2,RELAT_2:def 10 :: thesis: ( a in field (P \/ R) implies not [a,a] in P \/ R )
A3: now :: thesis: ( a in field P implies not [a,a] in P \/ R )
assume a in field P ; :: thesis: not [a,a] in P \/ R
then A4: not [a,a] in P by A1;
A5: ( 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 A2;
hence not [a,a] in P \/ R by A4, A5, XBOOLE_0:def 3; :: thesis: verum
end;
A6: now :: thesis: ( a in field R implies not [a,a] in P \/ R )
assume a in field R ; :: thesis: not [a,a] in P \/ R
then A7: not [a,a] in R by A2;
A8: ( 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 A1;
hence not [a,a] in P \/ R by A7, A8, 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 A3, A6, XBOOLE_0:def 3; :: thesis: verum