Axiom ax_cho | index | src |

选择公理

axiom ax_cho {u w x y z: set}:
  $ \fo x \ex y \fo z (z \in x \and \ex u u \in z \imp
    \exu u (u \in z \and \exin{w}{y} (z \in w \and u \in w))) $;