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