diff --git a/CHANGES.md b/CHANGES.md
index b9138ee..2bd5edb 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -11,7 +11,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
 - Impred: Set constructor o for quantifying over propositions
 - Epsilon: Hilbert's ε operator
 - List: add iota and indexes
-- Set: add ι:Set
+- Set: add ι:Set and an axiom el:Π a,τ a saying that every set is non-empty 
 - Pos, Z: add printing to decimal notation
 
 ### Changed
diff --git a/Set.lp b/Set.lp
index 086e526..891ba8c 100644
--- a/Set.lp
+++ b/Set.lp
@@ -10,6 +10,10 @@ injective symbol τ : Set → TYPE; // `t or \tau
 
 builtin "T" ≔ τ;
 
+// We assume that sets are non-empty
+
+symbol el a : τ a;
+
 // Cartesian product
 
 constant symbol × : Set → Set → Set; notation × infix right 10; // \times