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 )
thus ( R | X = {} implies dom R misses X ) :: thesis: ( dom R misses X implies R | X = {} )

proof

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

proof

thus (dom R) /\ X c= {} :: according to XBOOLE_0:def 10 :: thesis: {} c= (dom R) /\ X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (dom R) /\ X or x in {} )
assume A2: x in (dom R) /\ X ; :: thesis: x in {}
then x in dom R by XBOOLE_0:def 4;
then A3: ex y being object st [x,y] in R by XTUPLE_0:def 12;
x in X by A2, XBOOLE_0:def 4;
hence x in {} by A1, A3, Def9; :: thesis: verum

end;

thus {} c= (dom R) /\ X ; :: thesis: verum

end;

end;

assume A4: (dom R) /\ X = {} ; :: according to XBOOLE_0:def 7 :: thesis: R | X = {}
let x be object ; :: according to RELAT_1:def 2 :: thesis: for b being object holds
( [x,b] in R | X iff [x,b] in {} )
let y be object ; :: thesis: ( [x,y] in R | X iff [x,y] in {} )

hereby :: thesis: ( [x,y] in {} implies [x,y] in R | X )

assume A5: [x,y] in R | X ; :: thesis: [x,y] in {}
then x in X by Def9;
then A6: not x in dom R by A4, XBOOLE_0:def 4;
[x,y] in R by A5, Def9;
hence [x,y] in {} by A6, XTUPLE_0:def 12; :: thesis: verum

end;

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