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

proof

assume y in R .: D1 ; :: thesis: ex x being Element of D st
( [x,y] in R & x in D1 )
then consider x being object such that
A1: [x,y] in R and
A2: x in D1 by RELAT_1:def 13;
reconsider a = x as Element of D by A1, ZFMISC_1:87;
take a ; :: thesis: ( [a,y] in R & a in D1 )
thus ( [a,y] in R & a in D1 ) by A1, A2; :: thesis: verum

end;

given x being Element of D such that A3: ( [x,y] in R & x in D1 ) ; :: thesis: y in R .: D1
thus y in R .: D1 by A3, RELAT_1:def 13; :: thesis: verum