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 axiom Eps_i_ax: !p:set prop.!x:set.p x -> p (Eps_i p) const Empty : set const Power : set set lemma !P:prop.Eps_i (\x:set.x = Empty | P) = Empty | P -> Power Empty != Empty | P -> Eps_i (\x:set.x != Empty | P) != Empty | P -> P | ~ P var P:prop hyp Eps_i (\x:set.x = Empty | P) = Empty | P claim Power Empty != Empty | P -> P | ~ P