正則性の公理

以下は,証明が省略された定理として,記述されていますが,正則性の公理として
知られるものです。
theorem
 x in X implies ex Y st Y in X & not ex x st x in X & x in Y;

記号論理で書けば, 任意の$X$に対して

$$(x \in X ) \Rightarrow (\exists Y) ( Y \in X \ and \ not (\exists x)( x \in X \ and \ x \in Y))$$

を表しています。$x$が集合$X$の要素であれば,集合$X$の要素であって, しかも,$x$をその要素として含むような$Y$は存在しないという主張を 表しています。