const setsum : set set set const ap : set set set const Empty : set const ordsucc : set set term pair_p = \x:set.setsum (ap x Empty) (ap x (ordsucc Empty)) = x axiom pair_ap_1: !x:set.!y:set.ap (setsum x y) (ordsucc Empty) = y axiom pair_ap_0: !x:set.!y:set.ap (setsum x y) Empty = x claim !x:set.!y:set.pair_p (setsum x y)