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

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