:: deftheorem Def9 defines surreal-valued SURREALC:def 9 :
for f being Function holds
( f is surreal-valued iff rng f is surreal-membered );