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 )

thus y in R .: D1 by A3, RELAT_1:def 13; :: thesis: verum

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

given x being Element of D such that A3:
( [x,y] in R & x in D1 )
; :: thesis: y in R .: D1
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;( [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

thus y in R .: D1 by A3, RELAT_1:def 13; :: thesis: verum