const ordinal : set prop const omega : set axiom omega_ordinal: ordinal omega const ordsucc : set set axiom ordinal_ordsucc: !x:set.ordinal x -> ordinal (ordsucc x) claim ordinal (ordsucc omega)