const In : set set prop term iIn = In infix iIn 2000 2000 const omega : set const equip : set set prop term finite = \x:set.?y:set.y iIn omega & equip x y const nat_p : set prop const Empty : set axiom nat_0: nat_p Empty axiom nat_p_omega: !x:set.nat_p x -> x iIn omega axiom equip_ref: !x:set.equip x x claim ?x:set.x iIn omega & equip Empty x