const In : set set prop term iIn = In infix iIn 2000 2000 const Sigma : set (set set) set const setsum : set set set axiom lamE: !x:set.!f:set set.!y:set.y iIn Sigma x f -> ?z:set.z iIn x & ?w:set.w iIn f z & y = setsum z w claim !x:set.!f:set set.!y:set.y iIn Sigma x (\z:set.f z) -> ?z:set.z iIn x & ?w:set.w iIn f z & y = setsum z w