let X be set ; :: thesis: for y being object
for R being Relation holds
( y in R .: X iff ex x being object st
( x in dom R & [x,y] in R & x in X ) )
let y be object ; :: thesis: for R being Relation holds
( y in R .: X iff ex x being object st
( x in dom R & [x,y] in R & x in X ) )
let R be Relation; :: thesis: ( y in R .: X iff ex x being object st
( x in dom R & [x,y] in R & x in X ) )
thus ( y in R .: X implies ex x being object st
( x in dom R & [x,y] in R & x in X ) ) :: thesis: ( ex x being object st
( x in dom R & [x,y] in R & x in X ) implies y in R .: X )

proof

assume y in R .: X ; :: thesis: ex x being object st
( x in dom R & [x,y] in R & x in X )
then consider x being object such that
A1: ( [x,y] in R & x in X ) by Def11;
take x ; :: thesis: ( x in dom R & [x,y] in R & x in X )
thus ( x in dom R & [x,y] in R & x in X ) by A1, XTUPLE_0:def 12; :: thesis: verum

end;

thus ( ex x being object st
( x in dom R & [x,y] in R & x in X ) implies y in R .: X ) by Def11; :: thesis: verum