diff --git a/Nevanlinna/meromorphicOn.lean b/Nevanlinna/meromorphicOn.lean
index ac66cb9..d88a1c9 100644
--- a/Nevanlinna/meromorphicOn.lean
+++ b/Nevanlinna/meromorphicOn.lean
@@ -14,13 +14,14 @@ theorem MeromorphicOn.order_ne_top
   {U : Set ℂ}
   (h₁U : IsConnected U)
   (h₁f : MeromorphicOn f U) :
-  (∃ z₀ : U, (h₁f z₀.1 z₀.2).order ≠ ⊤) ↔ (∀ z : U, (h₁f z.1 z.2).order ≠ ⊤) := by
+  (∃ z₀ : U, (h₁f z₀.1 z₀.2).order = ⊤) ↔ (∀ z : U, (h₁f z.1 z.2).order = ⊤) := by
 
   constructor
   · intro h
     obtain ⟨h₁z₀, h₂z₀⟩ := h
     intro hz
 
+
     sorry
 
   · intro h
diff --git a/Nevanlinna/stronglyMeromorphicOn_eliminate.lean b/Nevanlinna/stronglyMeromorphicOn_eliminate.lean
index 691fc76..a63406a 100644
--- a/Nevanlinna/stronglyMeromorphicOn_eliminate.lean
+++ b/Nevanlinna/stronglyMeromorphicOn_eliminate.lean
@@ -10,16 +10,6 @@ import Nevanlinna.mathlibAddOn
 open scoped Interval Topology
 open Real Filter MeasureTheory intervalIntegral
 
-theorem MeromorphicOn.order_ne_top
-  {f : ℂ → ℂ}
-  {U : Set ℂ}
-  (h₁U : IsConnected U)
-  (h₂U : IsCompact U)
-  (h₁f : MeromorphicOn f U)
-  (h₂f : ∃ z₀ ∈ U, f z₀ ≠ 0) :
-  ∀ hz : z ∈ U, (h₁f z hz).order ≠ ⊤ := by
-
-  sorry
 
 
 theorem MeromorphicOn.decompose