:: deftheorem Def4 defines Ordinal-yielding ORDINAL2:def 4 :
for f being Function holds
( f is Ordinal-yielding iff ex A being Ordinal st rng f c= A );