--- a/zf.agda	Sun Jun 02 15:12:26 2019 +0900
+++ b/zf.agda	Mon Jun 03 10:19:52 2019 +0900
@@ -53,6 +53,8 @@
   A ∩ B = Select A (  λ x → ( A ∋ x ) ∧ ( B ∋ x )  )
   _∪_ : ( A B : ZFSet  ) → ZFSet
   A ∪ B = Union (A , B) 
+  ｛_｝ : ZFSet → ZFSet
+  ｛ x ｝ = ( x ,  x )
   infixr  200 _∈_
   infixr  230 _∩_ _∪_
   infixr  220 _⊆_ 
@@ -68,7 +70,7 @@
      regularity : ∀( x : ZFSet  ) → (not : ¬ (x ≈ ∅)) → (  minimul x not  ∈ x ∧  (  minimul x not  ∩ x  ≈ ∅ ) )
      -- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) )
      infinity∅ :  ∅ ∈ infinite
-     infinity :  ∀( X x : ZFSet  ) → x ∈ infinite →  ( x ∪ Select X (  λ y → x ≈ y )) ∈ infinite 
+     infinity :  ∀( X x : ZFSet  ) → x ∈ infinite →  ( x ∪ ｛ x ｝) ∈ infinite 
      selection : { ψ : ZFSet → Set m } → ∀ { X y : ZFSet  } →  ( ( y ∈ X ) ∧ ψ y ) ⇔ (y ∈  Select X ψ ) 
      -- replacement : ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) )
      replacement : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet  ) →  ( ψ x ∈  Replace X ψ )