Set: add axiom saying that sets are non-empty (#27)

Author: fblanqui

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

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