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 and
A2: y in Y and
A3: x in Im ((R ~),y) ; :: thesis: Y meets R .: X
consider a being object such that
A4: [a,x] in R ~ and
A5: a in {y} by A3, RELAT_1:def 13;
a = y by A5, TARSKI:def 1;
then [x,y] in R by A4, RELAT_1:def 7;
then y in R .: X by A1, RELAT_1:def 13;
hence Y meets R .: X by A2, 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 object such that
A6: a in Y and
A7: a in R .: X by XBOOLE_0:3;
consider b being object such that
A8: [b,a] in R and
A9: b in X by A7, RELAT_1:def 13;
A10: [a,b] in R ~ by A8, RELAT_1:def 7;
A11: a in {a} by TARSKI:def 1;
reconsider a = a, b = b as set by TARSKI: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 A9; :: thesis: ( a in Y & b in Im ((R ~),a) )
thus a in Y by A6; :: thesis: b in Im ((R ~),a)
thus b in Im ((R ~),a) by A10, A11, RELAT_1:def 13; :: thesis: verum