const In : set set prop term iIn = In infix iIn 2000 2000 const Subq : set set prop term TransSet = \x:set.!y:set.y iIn x -> Subq y x axiom Subq_ref: !x:set.Subq x x const ordsucc : set set axiom ordsuccE: !x:set.!y:set.y iIn ordsucc x -> y iIn x | y = x claim !x:set.!y:set.TransSet y -> x iIn ordsucc y -> Subq x y