let y, X be set ; :: thesis: for R being Relation holds
( y in R .: X iff ex x being set 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 set st
( x in dom R & [x,y] in R & x in X ) )
thus ( y in R .: X implies ex x being set st
( x in dom R & [x,y] in R & x in X ) ) :: thesis: ( ex x being set 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 set st
( x in dom R & [x,y] in R & x in X )
then consider x being set such that
A1: ( [x,y] in R & x in X ) by Def13;
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, Def4; :: thesis: verum

end;

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