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