let R1, R2 be 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 ) ) )
let x, y be set ; ( 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 ) )
( ( 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
;
MMLQUERY:def 1 ( 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 ) )
;
verum
end;
assume
( x,y in R1 or ( y,x nin R1 & x,y in R2 ) )
; 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; MMLQUERY:def 1 verum