Nicer proof "finished" (up to arithmetical facts).

[helm.git] / helm / software / matita / nlibrary / sets / sets.ma

diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma
index 3e63bf8f2574fee8eba104a243c6176e83832e39..4579054c5bd13096635804a796196d57a4a092e5 100644 (file)
--- a/helm/software/matita/nlibrary/sets/sets.ma
+++ b/helm/software/matita/nlibrary/sets/sets.ma
@@ -226,6 +226,7 @@ nqed.
 
 nrecord isomorphism (A) (B) (S: qpowerclass A) (T: qpowerclass B) : CProp[0] ≝
  { iso_f:> unary_morphism A B;
+   f_closed: ∀x. x ∈ S → iso_f x ∈ T;
    f_sur: surjective ?? S T iso_f;
    f_inj: injective ?? S iso_f
  }.