let z be set ; MMLQUER2:def 2 for y being set st z,y in R1 \, R2 & y,z in R1 \, R2 holds
z = y
let y be set ; ( z,y in R1 \, R2 & y,z in R1 \, R2 implies z = y )
assume A1:
( [z,y] in R1 \, R2 & [y,z] in R1 \, R2 )
; MMLQUERY:def 1 z = y
( z,y in R1 \, R2 & y,z in R1 \, R2 )
by A1;
then
( ( z,y in R1 or ( y,z nin R1 & z,y in R2 ) ) & ( y,z in R1 or ( z,y nin R1 & y,z in R2 ) ) )
by Th9;
then
( ( [z,y] in R1 & [y,z] in R1 ) or ( [z,y] in R2 & [y,z] in R2 ) )
;
then
( ( [z,y] in R1 & [y,z] in R1 & y in field R1 & z in field R1 ) or ( [z,y] in R2 & [y,z] in R2 & y in field R2 & z in field R2 ) )
by RELAT_1:15;
hence
y = z
by RELAT_2:def 4, RELAT_2:def 12; verum