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

proof

set E = (rng f) \/ REAL;
reconsider X = rng f as Subset of ((rng f) \/ REAL) by XBOOLE_1:7;
reconsider Y = REAL as Subset of ((rng f) \/ REAL) by XBOOLE_1:7;
assume rng f is real-membered ; :: thesis: f is real-valued
then for x being Element of (rng f) \/ REAL st x in rng f holds
x in REAL by XREAL_0:def 1;
then X c= Y by SUBSET_1:2;
hence f is real-valued by VALUED_0:def 3; :: thesis: verum

end;

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