let f be empty set ; :: thesis: f is Ordinal-yielding
take 0 ; :: according to ORDINAL2:def 8 :: thesis: rng f c= 0
thus rng f c= 0 ; :: thesis: verum