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 and
A2: a in (R ~ ) .: Y by XBOOLE_0:3;
consider b being set such that
A3: [b,a] in R ~ and
A4: b in Y by A2, RELAT_1:def 13;
A5: b in {b} by 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 A4; :: thesis: a in Im (R ~ ),b
thus a in Im (R ~ ),b by A3, A5, RELAT_1:def 13; :: thesis: verum

end;

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