const SNo_pair : set set set const Empty : set const ordsucc : set set term Complex_i = SNo_pair Empty (ordsucc Empty) const In : set set prop term iIn = In infix iIn 2000 2000 const real : set axiom real_0: Empty iIn real axiom real_1: ordsucc Empty iIn real const complex : set axiom complex_I: !x:set.x iIn real -> !y:set.y iIn real -> SNo_pair x y iIn complex claim Complex_i iIn complex