thus ex a being ordinal number st rng f c= a by ORDINAL2:def 8; :: according to ORDINAL6:def 1 :: thesis: verum