const binunion : set set set const Sing : set set term SetAdjoin = \x:set.\y:set.binunion x (Sing y) const ordinal : set prop const In : set set prop term iIn = In infix iIn 2000 2000 axiom ordinal_Hered: !x:set.ordinal x -> !y:set.y iIn x -> ordinal y const ordsucc : set set const Empty : set axiom not_ordinal_Sing1: ~ ordinal (Sing (ordsucc Empty)) var x:set hyp ordinal (SetAdjoin x (Sing (ordsucc Empty))) claim ~ Sing (ordsucc Empty) iIn SetAdjoin x (Sing (ordsucc Empty))