let f be Relation; :: thesis: ( f is REAL -valued iff rng f is real-membered )
( f is REAL -valued iff f is real-valued ) ;
hence ( f is REAL -valued iff rng f is real-membered ) by RV; :: thesis: verum