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