let X be set ; :: thesis: for R being Relation holds
( R | X = {} iff dom R misses X )
let R be Relation; :: thesis: ( R | X = {} iff dom R misses X )

hereby :: thesis: ( dom R misses X implies R | X = {} )

assume A1: R | X = {} ; :: thesis: dom R misses X

now

let x be set ; :: thesis: ( x in (dom R) /\ X iff x in {} )

now

assume A2: x in (dom R) /\ X ; :: thesis: contradiction
then x in dom R by XBOOLE_0:def 4;
then A3: ex y being set st [x,y] in R by Def4;
x in X by A2, XBOOLE_0:def 4;
hence contradiction by A1, A3, Def11; :: thesis: verum

end;

hence ( x in (dom R) /\ X iff x in {} ) ; :: thesis: verum

end;

then (dom R) /\ X = {} by TARSKI:2;
hence dom R misses X by XBOOLE_0:def 7; :: thesis: verum

end;

assume A4: (dom R) /\ X = {} ; :: according to XBOOLE_0:def 7 :: thesis: R | X = {}

now

let x, y be set ; :: thesis: ( [x,y] in R | X iff [x,y] in {} )

now

assume A5: [x,y] in R | X ; :: thesis: contradiction
then x in X by Def11;
then A6: not x in dom R by A4, XBOOLE_0:def 4;
[x,y] in R by A5, Def11;
hence contradiction by A6, Def4; :: thesis: verum

end;

hence ( [x,y] in R | X iff [x,y] in {} ) ; :: thesis: verum

end;

hence R | X = {} by Def2; :: thesis: verum