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 )

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

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;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

A6: now :: thesis: ( a in field R implies not [a,a] in P \/ R )

assume
a in field (P \/ R)
; :: thesis: not [a,a] in P \/ Rassume
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;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

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