const In : set set prop term iIn = In infix iIn 2000 2000 term nIn = \x:set.\y:set.~ x iIn y const Eps_i : (set prop) set const Empty : set var P:prop hyp Eps_i (\x:set.x = Empty | P) = Empty hyp Eps_i (\x:set.x != Empty | P) != Empty hyp P claim (\x:set.x = Empty | P) != \x:set.x != Empty | P