const Eps_i : (set prop) set term If_i = \P:prop.\x:set.\y:set.Eps_i \z:set.P & z = x | ~ P & z = y axiom xm: !P:prop.P | ~ P lemma !P:prop.!x:set.!y:set.P -> P & x = x | ~ P & x = y -> P & Eps_i (\z:set.P & z = x | ~ P & z = y) = x | ~ P & Eps_i (\z:set.P & z = x | ~ P & z = y) = y lemma !P:prop.!x:set.!y:set.~ P -> P & y = x | ~ P & y = y -> P & Eps_i (\z:set.P & z = x | ~ P & z = y) = x | ~ P & Eps_i (\z:set.P & z = x | ~ P & z = y) = y claim !P:prop.!x:set.!y:set.P & If_i P x y = x | ~ P & If_i P x y = y