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