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
assume not dom R misses X ; :: thesis: contradiction
then consider x being set such that
A2: ( x in dom R & x in X ) by XBOOLE_0:3;
consider y being set such that
A3: [x,y] in R by A2, Def4;
thus contradiction by A1, A2, A3, Th143; :: thesis: verum

end;

assume A4: (dom R) /\ X = {} ; :: according to XBOOLE_0:def 7 :: thesis: R .: X = {}
consider y being Element of R .: X;
assume not R .: X = {} ; :: thesis: contradiction
then consider x being set such that
A5: ( x in dom R & [x,y] in R & x in X ) by Th143;
thus contradiction by A4, A5, XBOOLE_0:def 4; :: thesis: verum