diff --git a/Lattice.agda b/Lattice.agda
index dbe0ade..ae7035f 100644
--- a/Lattice.agda
+++ b/Lattice.agda
@@ -103,6 +103,15 @@ record IsSemilattice {a} (A : Set a)
         , λ a₂≈a₄ → a₁̷≈a₃ (≈-trans a₁≈a₂ (≈-trans a₂≈a₄ (≈-sym a₃≈a₄)))
         )
 
+module _ {a} {A : Set a}
+         {_≈_ : A → A → Set a} {_⊔_ : A → A → A}
+         (lA : IsSemilattice A _≈_ _⊔_) where
+
+    open IsSemilattice lA using (_≼_)
+
+    id-Mono : Monotonic _≼_ _≼_ (λ x → x)
+    id-Mono a₁≼a₂ = a₁≼a₂
+
 module _ {a b} {A : Set a} {B : Set b}
          {_≈₁_ : A → A → Set a} {_⊔₁_ : A → A → A}
          {_≈₂_ : B → B → Set b} {_⊔₂_ : B → B → B}