let x, y be object ; :: thesis: for A, B being set
for R being Subset of [:A,B:] holds
( y in Im ((R `),x) iff ( not [x,y] in R & x in A & y in B ) )
let A, B be set ; :: thesis: for R being Subset of [:A,B:] holds
( y in Im ((R `),x) iff ( not [x,y] in R & x in A & y in B ) )
let R be Subset of [:A,B:]; :: thesis: ( y in Im ((R `),x) iff ( not [x,y] in R & x in A & y in B ) )
thus ( y in Im ((R `),x) implies ( not [x,y] in R & x in A & y in B ) ) :: thesis: ( not [x,y] in R & x in A & y in B implies y in Im ((R `),x) )

proof

assume y in Im ((R `),x) ; :: thesis: ( not [x,y] in R & x in A & y in B )
then ex a being object st
( [a,y] in R ` & a in {x} ) by RELAT_1:def 13;
then [x,y] in [:A,B:] \ R by TARSKI:def 1;
hence ( not [x,y] in R & x in A & y in B ) by XBOOLE_0:def 5, ZFMISC_1:87; :: thesis: verum

end;

assume that
A1: not [x,y] in R and
A2: x in A and
A3: y in B ; :: thesis: y in Im ((R `),x)
A4: x in {x} by TARSKI:def 1;
[x,y] in [:A,B:] by A2, A3, ZFMISC_1:87;
then [x,y] in [:A,B:] \ R by A1, XBOOLE_0:def 5;
hence y in Im ((R `),x) by A4, RELAT_1:def 13; :: thesis: verum