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 set such that
A2: y in rng R and
A3: y in Y by XBOOLE_0:3;
ex x being set st [x,y] in R by A2, Def5;
hence contradiction by A1, A2, A3, Th166; :: 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 set st
( y in rng R & [ the Element of R " Y,y] in R & y in Y ) by Th166;
hence contradiction by A4, XBOOLE_0:def 4; :: thesis: verum