Axiom ax_ac | index | src |

选择公理

axiom ax_ac {t u v w y z: set} (x: set):
  $ \ex y \fo z \fo w (z \in w \and w \in x \imp
    \ex v \fo u (\ex t (u \in w \and w \in t \and (u \in t \and t \in y)) \iff
      u = v)) $;