let P, R be Relation; :: thesis: (P \ R) ~ = (P ~ ) \ (R ~ )
for x, y being set holds
( [x,y] in (P \ R) ~ iff [x,y] in (P ~ ) \ (R ~ ) )

proof

let x, y be set ; :: thesis: ( [x,y] in (P \ R) ~ iff [x,y] in (P ~ ) \ (R ~ ) )
( [x,y] in (P \ R) ~ iff [y,x] in P \ R ) by Def7;
then ( [x,y] in (P \ R) ~ iff ( [y,x] in P & not [y,x] in R ) ) by XBOOLE_0:def 5;
then ( [x,y] in (P \ R) ~ iff ( [x,y] in P ~ & not [x,y] in R ~ ) ) by Def7;
hence ( [x,y] in (P \ R) ~ iff [x,y] in (P ~ ) \ (R ~ ) ) by XBOOLE_0:def 5; :: thesis: verum

end;

hence (P \ R) ~ = (P ~ ) \ (R ~ ) by Def2; :: thesis: verum