let Y be set ; :: thesis: for R being Relation holds
( R " Y = {} iff rng R misses Y )
let R be Relation; :: thesis: ( R " Y = {} iff rng R misses Y )
set x = the Element of R " Y;
thus ( R " Y = {} implies rng R misses Y ) :: thesis: ( rng R misses Y implies R " Y = {} )

proof

assume A1: R " Y = {} ; :: thesis: rng R misses Y
assume not rng R misses Y ; :: thesis: contradiction
then consider y being object such that
A2: y in rng R and
A3: y in Y by XBOOLE_0:3;
ex x being object st [x,y] in R by A2, XTUPLE_0:def 13;
hence contradiction by A1, A2, A3, Th123; :: thesis: verum

end;

assume A4: (rng R) /\ Y = {} ; :: according to XBOOLE_0:def 7 :: thesis: R " Y = {}
assume not R " Y = {} ; :: thesis: contradiction
then ex y being object st
( y in rng R & [ the Element of R " Y,y] in R & y in Y ) by Th123;
hence contradiction by A4, XBOOLE_0:def 4; :: thesis: verum