update in ground

[helm.git] / matita / matita / contribs / lambdadelta / ground / lib / subset.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/lib/subset.ma b/matita/matita/contribs/lambdadelta/ground/lib/subset.ma
index 25863fe2b6f8547929aaae653dbbf0d93c5d983a..8f0154d813dd6ef8b96042b35a9b7c2915c377f1 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/lib/subset.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/subset.ma
@@ -12,9 +12,10 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "ground/lib/relations.ma".
 include "ground/notation/functions/powerclass_1.ma".
 include "ground/notation/relations/epsilon_3.ma".
-include "ground/lib/relations.ma".
+include "ground/notation/relations/not_epsilon_3.ma".
 
 (* SUBSETS ******************************************************************)
 
@@ -31,3 +32,7 @@ definition subset_in (A): 𝒫❨A❩ → 𝒫❨A❩ ≝
 interpretation
   "membership (subset)"
   'Epsilon A a u = (subset_in A u a).
+
+interpretation
+  "negated membership (subset)"
+  'NotEpsilon A a u = (negation (subset_in A u a)).