Fix broken proof because of d6d78d9

Because `open_neighborhood` gets unfolded by `intuition`, the proof ends
earlier than the proof-script anticipated. This error was caused because
I didn't check whether the repo still compiles…

Author: Columbus240

theories/Topology/Neighborhoods.v

@@ -50,7 +50,7 @@ Lemma open_char_neighborhood: forall {X:TopologicalSpace} (U : Ensemble X),
 Proof.
   split.
   - intros.
-    exists U. intuition. red. intuition.
+    exists U. intuition.
   - intros.
     assert (U = FamilyUnion (fun V => open V /\ Included V U)).
     2: {