--- a/src/Topology.agda	Tue Mar 07 19:19:03 2023 +0900
+++ b/src/Topology.agda	Wed Mar 08 10:28:55 2023 +0900
@@ -224,12 +224,14 @@
 -- Product Topology is not
 --     ZFP (OS TP) (OS TQ) (box)
 
+-- Rectangle subset (zπ1 ⁻¹ p)
 record BaseP {P : HOD} (TP : Topology P ) (Q : HOD) (x : Ordinal) : Set n where
    field
        p : Ordinal
        op : odef (OS TP) p
        prod : x ≡ & (ZFP (* p) Q )
 
+-- Rectangle subset (zπ12⁻¹ q )
 record BaseQ (P : HOD) {Q : HOD} (TQ : Topology Q ) (x : Ordinal) : Set n where
    field
        q  : Ordinal
@@ -287,7 +289,7 @@
 
 data Finite-∪ (S : HOD) : Ordinal → Set n where
    fin-e : Finite-∪ S o∅
-   fin-i : {x : Ordinal } → odef S x  → Finite-∪ S (& ( * x , * x ))
+   fin-i : {x : Ordinal } → odef S x  → Finite-∪ S (& ( * x , * x ))   -- an element of S
    fin-∪ : {x y : Ordinal } → Finite-∪ S x → Finite-∪ S y → Finite-∪ S (& (* x ∪ * y))
    --  Finite-∪ S y → Union y ⊆ S
 
@@ -621,8 +623,9 @@
 
 open Filter
 
--- Ultra Filter has limit point
-
+--
+-- {v | Neighbor lim v}  set of u ⊆ v ⊆ P where u is an open set u ∋ x
+--
 record Neighbor {P : HOD} (TP : Topology P) (x v : Ordinal) : Set n where
    field
        u : Ordinal