diff --git a/Lattice/Builder.agda b/Lattice/Builder.agda
index 7aaeec3..f9f2374 100644
--- a/Lattice/Builder.agda
+++ b/Lattice/Builder.agda
@@ -124,7 +124,10 @@ record IsPartialSemilattice {a} {A : Set a}
         field
             x : A
             not-partial : ∀ (a₁ a₂ : A) →  Σ A (λ a₃ →  (a₁ ⊔? a₂) ≡ just a₃)
-            x-identity : (a : A) → (x ⊔? a) ≈? just a
+            x-identityˡ : (a : A) → (x ⊔? a) ≈? just a
+
+        x-identityʳ : (a : A) → (a ⊔? x) ≈? just a
+        x-identityʳ a = ≈?-trans (⊔-comm a x) (x-identityˡ a)
 
 Maybe-≈ : ∀ {a} {A : Set a} → (_≈_ : A → A → Set a) → Maybe A →  A → Set a
 Maybe-≈ _≈_ (just a₁) a₂ = a₁ ≈ a₂