const ordinal : set prop const In : set set prop term iIn = In infix iIn 2000 2000 var p:set prop hyp ?x:set.ordinal x & p x hyp ~ ?x:set.ordinal x & p x & !y:set.y iIn x -> ~ p y claim ~ !x:set.ordinal x -> ~ p x