const In : set set prop term iIn = In infix iIn 2000 2000 term Subq = \x:set.\y:set.!z:set.z iIn x -> z iIn y const Empty : set const real : set axiom real_0: Empty iIn real const SNo_pair : set set set const complex : set axiom complex_I: !x:set.x iIn real -> !y:set.y iIn real -> SNo_pair x y iIn complex axiom SNo_pair_0: !x:set.SNo_pair x Empty = x claim !x:set.x iIn real -> x iIn complex