let A, B be set ; :: thesis: for R being Subset of [:A,B:]
for X, Y being set holds
( ex x, y being set st
( x in X & y in Y & x in Im (R ~ ),y ) iff Y meets R .: X )
let R be Subset of [:A,B:]; :: thesis: for X, Y being set holds
( ex x, y being set st
( x in X & y in Y & x in Im (R ~ ),y ) iff Y meets R .: X )
let X, Y be set ; :: thesis: ( ex x, y being set st
( x in X & y in Y & x in Im (R ~ ),y ) iff Y meets R .: X )
thus ( ex x, y being set st
( x in X & y in Y & x in Im (R ~ ),y ) implies Y meets R .: X ) :: thesis: ( Y meets R .: X implies ex x, y being set st
( x in X & y in Y & x in Im (R ~ ),y ) )

proof

given x, y being set such that A1: ( x in X & y in Y & x in Im (R ~ ),y ) ; :: thesis: Y meets R .: X
consider a being set such that
A2: ( [a,x] in R ~ & a in {y} ) by A1, RELAT_1:def 13;
a = y by A2, TARSKI:def 1;
then ( [x,y] in R & x in X ) by A1, A2, RELAT_1:def 7;
then y in R .: X by RELAT_1:def 13;
hence Y meets R .: X by A1, XBOOLE_0:3; :: thesis: verum

end;

assume Y meets R .: X ; :: thesis: ex x, y being set st
( x in X & y in Y & x in Im (R ~ ),y )
then consider a being set such that
A3: ( a in Y & a in R .: X ) by XBOOLE_0:3;
consider b being set such that
A4: ( [b,a] in R & b in X ) by A3, RELAT_1:def 13;
A5: ( [a,b] in R ~ & a in {a} ) by A4, RELAT_1:def 7, TARSKI:def 1;
take b ; :: thesis: ex y being set st
( b in X & y in Y & b in Im (R ~ ),y )
take a ; :: thesis: ( b in X & a in Y & b in Im (R ~ ),a )
thus b in X by A4; :: thesis: ( a in Y & b in Im (R ~ ),a )
thus a in Y by A3; :: thesis: b in Im (R ~ ),a
thus b in Im (R ~ ),a by A5, RELAT_1:def 13; :: thesis: verum