--- a/src/Topology.agda	Wed Feb 22 12:01:09 2023 +0900
+++ b/src/Topology.agda	Thu Feb 23 09:58:11 2023 +0800
@@ -279,12 +279,19 @@
 
 fipx : {L : HOD} (top : Topology L) → {X : Ordinal } → * X ⊆ CS top
      →   ( { C : Ordinal  } { x : Ordinal } → * C ⊆ * X → Subbase (* C) x → o∅ o< x ) →  Ordinal
-fipx {L} top {X} X⊆CS fip with fip (λ x → x) (gi ?)
-... | t = ?
+fipx {L} top {X} X⊆CS fip with trio< X o∅ 
+... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
+... | tri≈ ¬a b ¬c = o∅
+... | tri> ¬a ¬b c = & (ODC.minimal O (* fip00) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) ( fip (λ x → x ) (gi ? ) )))) where
+   fip00 : ?
+   fip00 = & (ODC.minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) c ) )) 
 
 fipX∋x : {L : HOD} (top : Topology L) → {X : Ordinal } → (X⊆CS : * X ⊆ CS top )
      →   (fip : { C : Ordinal  } { x : Ordinal } → * C ⊆ * X → Subbase (* C) x → o∅ o< x ) →  odef (* X) (fipx top X⊆CS fip)
-fipX∋x = ?
+fipX∋x {L} top {X} X⊆CS fip with trio< X o∅ 
+... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
+... | tri≈ ¬a b ¬c = ?
+... | tri> ¬a ¬b c = ? -- fip (λ x → x) (gi ?)
 
 -- Compact
 
@@ -468,7 +475,7 @@
    ... | record { z = z ; az = az ; x=ψz = x=ψz } =  subst (λ k → odef (OS top) k) (sym x=ψz) ( P＼CS=OS top (cs comp01))  where
        comp01 : odef (* X) (& (* z))
        comp01 = subst (λ k → odef (* X) k) (sym &iso) az
-   --
+
    --   if all finite intersection of (OX X) contains something, 
    --   there is no finite cover. From Compactness, (OX X) is not a cover of L ( contraposition of Compact)
    --     it means there is a limit

--- a/src/VL.agda	Wed Feb 22 12:01:09 2023 +0900
+++ b/src/VL.agda	Thu Feb 23 09:58:11 2023 +0800
@@ -57,7 +57,7 @@
 --
 -- Definition for Power Set
 --
-record Definitions  : Set (suc n) where
+record Definitions  : Set (suc n) where 
    field
       Definition : HOD → HOD