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