const pair_p : set prop const setsum : set set set axiom pair_p_I: !x:set.!y:set.pair_p (setsum x y) const ap : set set set const Empty : set axiom pair_ap_0: !x:set.!y:set.ap (setsum x y) Empty = x axiom exandE_i: !p:set prop.!q:set prop.(?x:set.p x & q x) -> !P:prop.(!x:set.p x -> q x -> P) -> P const In : set set prop term iIn = In infix iIn 2000 2000 const Sigma : set (set set) set var x:set var f:set set var y:set hyp y iIn Sigma x f claim (?z:set.z iIn x & ?w:set.w iIn f z & y = setsum z w) -> pair_p y & ap y Empty iIn x