const ordinal : set prop const SNo : set prop axiom ordinal_SNo: !x:set.ordinal x -> SNo x const Empty : set axiom ordinal_Empty: ordinal Empty const add_SNo : set set set term + = add_SNo infix + 2281 2280 const ordsucc : set set axiom add_SNo_ordinal_SL: !x:set.ordinal x -> !y:set.ordinal y -> ordsucc x + y = ordsucc (x + y) axiom add_SNo_0L: !x:set.SNo x -> Empty + x = x claim !x:set.ordinal x -> ordsucc x = ordsucc Empty + x