theorem Th9: :: MMLQUER2:9

for R1, R2 being Relation
for x, y being set holds
( x,y in R1 \, R2 iff ( x,y in R1 or ( y,x nin R1 & x,y in R2 ) ) )