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 )
assume A9: 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 A9, XBOOLE_0:def 4;
then not [a,a] in P by Def10, Def2;
hence not [a,a] in P /\ R by XBOOLE_0:def 4; :: thesis: verum