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