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 object such that
A1: a in X and
A2: a in (R ~) .: Y by XBOOLE_0:3;
consider b being object 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;
reconsider a = a, b = b as set by TARSKI: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 object 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