diff --git a/FiniteSets/misc/ordered.v b/FiniteSets/misc/ordered.v
index 46ab730..20981ec 100644
--- a/FiniteSets/misc/ordered.v
+++ b/FiniteSets/misc/ordered.v
@@ -155,6 +155,7 @@ Section min_set.
   Context `{TotalOrder A}.
   Context `{Univalence} `{IsHSet A}.
 
+  (* The reason why we put an additional element on top, is so that we can take the minimum of two results when considering union *)
   Definition min_set : FSet A -> Topped A.
   Proof.
     hrecursion.