let f be Relation; :: thesis: ( rng f is integer-membered iff f is INT -valued )
thus ( rng f is integer-membered implies f is INT -valued ) :: thesis: ( f is INT -valued implies rng f is integer-membered )

proof

set E = (rng f) \/ INT;
reconsider X = rng f as Subset of ((rng f) \/ INT) by XBOOLE_1:7;
reconsider Y = INT as Subset of ((rng f) \/ INT) by XBOOLE_1:7;
assume rng f is integer-membered ; :: thesis: f is INT -valued
then for x being Element of (rng f) \/ INT st x in rng f holds
x in INT by INT_1:def 2;
then X c= Y by SUBSET_1:2;
hence f is INT -valued by RELAT_1:def 19; :: thesis: verum

end;

thus ( f is INT -valued implies rng f is integer-membered ) ; :: thesis: verum