let z be set ; :: according to MMLQUER2:def 2 :: thesis: for y being set st z,y in R1 \, R2 & y,z in R1 \, R2 holds
z = y
let y be set ; :: thesis: ( 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 ) ; :: according to MMLQUERY:def 1 :: thesis: 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; :: thesis: verum