diff --git a/modules/FiniteSetsExtTheorems.tla b/modules/FiniteSetsExtTheorems.tla
index 6f22eb6..533e678 100644
--- a/modules/FiniteSetsExtTheorems.tla
+++ b/modules/FiniteSetsExtTheorems.tla
@@ -188,7 +188,7 @@ THEOREM ProductSetZero ==
 (* bounded by the product of the full set.                               *)
 (*************************************************************************)
 THEOREM ProductSetNatSubset ==
-    ASSUME NEW S \in SUBSET Nat \ {0}, IsFiniteSet(S),
+    ASSUME NEW S \in SUBSET (Nat \ {0}), IsFiniteSet(S),
            NEW T \in SUBSET S
     PROVE  ProductSet(T) <= ProductSet(S)
 
diff --git a/modules/FiniteSetsExtTheorems_proofs.tla b/modules/FiniteSetsExtTheorems_proofs.tla
index 29a3b28..2daa477 100644
--- a/modules/FiniteSetsExtTheorems_proofs.tla
+++ b/modules/FiniteSetsExtTheorems_proofs.tla
@@ -295,7 +295,7 @@ THEOREM ProductSetZero ==
   <2>. QED   BY DEF P
 
 THEOREM ProductSetNatSubset ==
-    ASSUME NEW S \in SUBSET Nat \ {0}, IsFiniteSet(S),
+    ASSUME NEW S \in SUBSET (Nat \ {0}), IsFiniteSet(S),
            NEW T \in SUBSET S
     PROVE  ProductSet(T) <= ProductSet(S)
 <1>. DEFINE U == S \ T
@@ -362,7 +362,7 @@ THEOREM MapThenSumSetAddElement ==
     ASSUME NEW S, IsFiniteSet(S), NEW x, x \notin S,
            NEW op(_), \A s \in S \union {x} : op(s) \in Int
     PROVE  MapThenSumSet(op, S \union {x}) = op(x) + MapThenSumSet(op, S)
-<1>. \A T \in SUBSET S \union {x} : T # {} => (CHOOSE t \in T : TRUE) \in T 
+<1>. \A T \in SUBSET (S \union {x}) : T # {} => (CHOOSE t \in T : TRUE) \in T 
   OBVIOUS
 <1>. /\ 0 \in Int 
      /\ \A i,j \in Int : i+j \in Int
diff --git a/modules/FoldsTheorems.tla b/modules/FoldsTheorems.tla
index a51f79c..c332071 100644
--- a/modules/FoldsTheorems.tla
+++ b/modules/FoldsTheorems.tla
@@ -102,7 +102,7 @@ THEOREM MapThenFoldSetACAddElement ==
            \A t,u \in Typ : op(t,u) = op(u,t),
            \A t,u,v \in Typ : op(t, op(u,v)) = op(op(t,u),v),
            NEW S, IsFiniteSet(S), NEW x, x \notin S,
-           NEW choose(_), \A T \in SUBSET S \union {x} : T # {} => choose(T) \in T,
+           NEW choose(_), \A T \in SUBSET (S \union {x}) : T # {} => choose(T) \in T,
            \A s \in S \union {x} : f(s) \in Typ
     PROVE  MapThenFoldSet(op, base, f, choose, S \union {x}) = 
            op(f(x), MapThenFoldSet(op, base, f, choose, S))
diff --git a/modules/FoldsTheorems_proofs.tla b/modules/FoldsTheorems_proofs.tla
index 68cca64..fba7852 100644
--- a/modules/FoldsTheorems_proofs.tla
+++ b/modules/FoldsTheorems_proofs.tla
@@ -271,7 +271,7 @@ THEOREM MapThenFoldSetACAddElement ==
            \A t,u \in Typ : op(t,u) = op(u,t),
            \A t,u,v \in Typ : op(t, op(u,v)) = op(op(t,u),v),
            NEW S, IsFiniteSet(S), NEW x, x \notin S,
-           NEW choose(_), \A T \in SUBSET S \union {x} : T # {} => choose(T) \in T,
+           NEW choose(_), \A T \in SUBSET (S \union {x}) : T # {} => choose(T) \in T,
            \A s \in S \union {x} : f(s) \in Typ
     PROVE  MapThenFoldSet(op, base, f, choose, S \union {x}) = 
            op(f(x), MapThenFoldSet(op, base, f, choose, S))