axiom FalseE: ~ False const ordinal : set prop const In : set set prop term iIn = In infix iIn 2000 2000 const ordsucc : set set axiom ordinal_ordsucc_In_eq: !x:set.!y:set.ordinal x -> y iIn x -> ordsucc y iIn x | x = ordsucc y axiom xm: !P:prop.P | ~ P claim !x:set.ordinal x -> (!y:set.y iIn x -> ordsucc y iIn x) | ?y:set.y iIn x & x = ordsucc y