let a be set ; :: according to RELAT_2:def 2,RELAT_2:def 10 :: 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 Def10, Def2;
hence not [a,a] in P /\ R by XBOOLE_0:def 4; :: thesis: verum