const In : set set prop term iIn = In infix iIn 2000 2000 const omega : set const SNoLe : set set prop term <= = SNoLe infix <= 2020 2020 const ap : set set set const add_SNo : set set set term + = add_SNo infix + 2281 2280 const ordsucc : set set const Empty : set var x:set var y:set var z:set hyp !w:set.w iIn omega -> ap x w <= ap y w & ap x w <= ap x (w + ordsucc Empty) & ap y (w + ordsucc Empty) <= ap y w hyp z iIn omega claim ordsucc z = z + ordsucc Empty -> ap x z <= ap y z & ap x z <= ap x (ordsucc z) & ap y (ordsucc z) <= ap y z