let X, Y be set ; :: thesis: for R being Relation of X,Y holds
( ( for y being set st y in Y holds
ex x being set st [x,y] in R ) iff rng R = Y )
let R be Relation of X,Y; :: thesis: ( ( for y being set st y in Y holds
ex x being set st [x,y] in R ) iff rng R = Y )
thus ( ( for y being set st y in Y holds
ex x being set st [x,y] in R ) implies rng R = Y ) :: thesis: ( rng R = Y implies for y being set st y in Y holds
ex x being set st [x,y] in R )

proof

assume A1: for y being set st y in Y holds
ex x being set st [x,y] in R ; :: thesis: rng R = Y
thus rng R = Y :: thesis: verum

proof

now

let y be set ; :: thesis: ( y in rng R iff y in Y )

now

assume y in Y ; :: thesis: y in rng R
then ex x being set st [x,y] in R by A1;
hence y in rng R by RELAT_1:20; :: thesis: verum

end;

hence ( y in rng R iff y in Y ) ; :: thesis: verum

end;

hence rng R = Y by TARSKI:2; :: thesis: verum

end;

end;

thus ( rng R = Y implies for y being set st y in Y holds
ex x being set st [x,y] in R ) by RELAT_1:def 5; :: thesis: verum