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

hereby :: thesis: ( ex x, y being set st
( x in X & y in Y & x in Im (R ~ ),y ) implies X meets (R ~ ) .: Y )

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

end;

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