let z be object ; RELAT_2:def 1,RELAT_2:def 9 ( not z in field (R1 \, R2) or [z,z] in R1 \, R2 )
assume
z in field (R1 \, R2)
; [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
; verum