const ordinal : set prop const Empty : set axiom ordinal_Empty: ordinal Empty const ordsucc : set set axiom ordinal_ordsucc: !x:set.ordinal x -> ordinal (ordsucc x) const nat_p : set prop axiom nat_ind: !p:set prop.p Empty -> (!x:set.nat_p x -> p x -> p (ordsucc x)) -> !x:set.nat_p x -> p x claim !x:set.nat_p x -> ordinal x