let z be object ; :: according to RELAT_2:def 1,RELAT_2:def 9 :: thesis: ( not z in field (R1 \, R2) or [z,z] in R1 \, R2 )
assume z in field (R1 \, R2) ; :: thesis: [z,z] in R1 \, R2
then z in (field R1) \/ (field R2) by Th10;
then ( z in field R1 or z in field R2 ) by XBOOLE_0:def 3;
then A1: ( [z,z] in R1 or ( [z,z] in R2 & [z,z] nin R1 ) ) by RELAT_2:def 1, RELAT_2:def 9;
reconsider zz = z as set by TARSKI:1;
( zz,zz in R1 or ( zz,zz in R2 & zz,zz nin R1 ) ) by A1;
then zz,zz in R1 \, R2 by Th9;
hence [z,z] in R1 \, R2 ; :: thesis: verum