Some notes by Giovanni.

[helm.git] / helm / software / matita / library / formal_topology / saturations_reductions.ma

diff --git a/helm/software/matita/library/formal_topology/saturations_reductions.ma b/helm/software/matita/library/formal_topology/saturations_reductions.ma
index d87ea9e1f4957cf9e6972e045254cc338df21e8f..0582bf0b1321d3188e2c9a0b4a914908bfd2843f 100644 (file)
--- a/helm/software/matita/library/formal_topology/saturations_reductions.ma
+++ b/helm/software/matita/library/formal_topology/saturations_reductions.ma
@@ -13,6 +13,7 @@
 (**************************************************************************)
 
 include "datatypes/subsets.ma".
+include "formal_topology/relations.ma".
 
 definition is_saturation ≝
  λC:REL.λA:unary_morphism (Ω \sup C) (Ω \sup C).