const Repl : set (set set) set const Sigma : set (set set) set term setprod = \x:set.\y:set.Sigma x \z:set.y const real : set const SNo_pair : set set set const ap : set set set const Empty : set const ordsucc : set set term complex = Repl (setprod real real) \x:set.SNo_pair (ap x Empty) (ap x (ordsucc Empty)) const In : set set prop term iIn = In infix iIn 2000 2000 axiom ap0_Sigma: !x:set.!f:set set.!y:set.y iIn Sigma x f -> ap y Empty iIn x axiom ap1_Sigma: !x:set.!f:set set.!y:set.y iIn Sigma x f -> ap y (ordsucc Empty) iIn f (ap y Empty) axiom ReplE_impred: !x:set.!f:set set.!y:set.y iIn Repl x f -> !P:prop.(!z:set.z iIn x -> y = f z -> P) -> P claim !x:set.x iIn complex -> !P:prop.(!y:set.y iIn real -> !z:set.z iIn real -> x = SNo_pair y z -> P) -> P