let D, D2, E be non empty set ; :: thesis: for R being Relation of D,E
for x being Element of D holds
( x in R " D2 iff ex y being Element of E st
( [x,y] in R & y in D2 ) )
let R be Relation of D,E; :: thesis: for x being Element of D holds
( x in R " D2 iff ex y being Element of E st
( [x,y] in R & y in D2 ) )
let x be Element of D; :: thesis: ( x in R " D2 iff ex y being Element of E st
( [x,y] in R & y in D2 ) )
thus ( x in R " D2 implies ex y being Element of E st
( [x,y] in R & y in D2 ) ) :: thesis: ( ex y being Element of E st
( [x,y] in R & y in D2 ) implies x in R " D2 )

proof

assume x in R " D2 ; :: thesis: ex y being Element of E st
( [x,y] in R & y in D2 )
then consider y being set such that
A1: ( [x,y] in R & y in D2 ) by RELAT_1:def 14;
reconsider b = y as Element of E by A1, ZFMISC_1:106;
take b ; :: thesis: ( [x,b] in R & b in D2 )
thus ( [x,b] in R & b in D2 ) by A1; :: thesis: verum

end;

given y being Element of E such that A2: ( [x,y] in R & y in D2 ) ; :: thesis: x in R " D2
thus x in R " D2 by A2, RELAT_1:def 14; :: thesis: verum