const nat_p : set prop const ordsucc : set set const Empty : set axiom nat_2: nat_p (ordsucc (ordsucc Empty)) const ordinal : set prop axiom nat_p_ordinal: !x:set.nat_p x -> ordinal x claim ordinal (ordsucc (ordsucc Empty))