const In : set set prop term iIn = In infix iIn 2000 2000 const ordsucc : set set axiom ordsuccI2: !x:set.x iIn ordsucc x const Empty : set claim Empty iIn ordsucc Empty