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 ;
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 ; :: thesis: verum