let R1, R2 be Relation; :: thesis: 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 ) ) )
let x, y be set ; :: thesis: ( x,y in R1 \, R2 iff ( x,y in R1 or ( y,x nin R1 & x,y in R2 ) ) )
set R = { [a,b] where a, b is Element of field R2 : ( b,a nin R1 & a,b in R2 ) } ;
thus ( not x,y in R1 \, R2 or x,y in R1 or ( y,x nin R1 & x,y in R2 ) ) :: thesis: ( ( x,y in R1 or ( y,x nin R1 & x,y in R2 ) ) implies x,y in R1 \, R2 )

proof

assume [x,y] in R1 \, R2 ; :: according to MMLQUERY:def 1 :: thesis: ( x,y in R1 or ( y,x nin R1 & x,y in R2 ) )
then ( [x,y] in R1 or [x,y] in R2 \ (R1 ~) ) by XBOOLE_0:def 3;
then ( [x,y] in R1 or ( [x,y] in R2 & not [x,y] in R1 ~ ) ) by XBOOLE_0:def 5;
then A1: ( [x,y] in R1 or ( [x,y] in R2 & not [y,x] in R1 ) ) by RELAT_1:def 7;
reconsider xx = x, yy = y as set ;
( xx,yy in R1 or ( xx,yy in R2 & not yy,xx in R1 ) ) by A1;
hence ( x,y in R1 or ( y,x nin R1 & x,y in R2 ) ) ; :: thesis: verum

end;

assume ( x,y in R1 or ( y,x nin R1 & x,y in R2 ) ) ; :: thesis: x,y in R1 \, R2
then ( [x,y] in R1 or ( [x,y] in R2 & not [y,x] in R1 ) ) ;
then ( [x,y] in R1 or ( [x,y] in R2 & not [x,y] in R1 ~ ) ) by RELAT_1:def 7;
then ( [x,y] in R1 or [x,y] in R2 \ (R1 ~) ) by XBOOLE_0:def 5;
hence [x,y] in R1 \, R2 by XBOOLE_0:def 3; :: according to MMLQUERY:def 1 :: thesis: verum