diff --git a/doc/lean/tutorial.org b/doc/lean/tutorial.org
index 2993bff273..0538e59f8b 100644
--- a/doc/lean/tutorial.org
+++ b/doc/lean/tutorial.org
@@ -233,7 +233,7 @@ What is the type of =Type=?
   check Type
 #+END_SRC
 
-Lean reports =Type : Type=, is it Lean inconsistent? Now, it is not.
+Lean reports =Type : Type=, is Lean inconsistent? No, it is not.
 Internally, Lean maintains a hierarchy of Types. We say each one of
 them _lives_ in a universe. Lean is universe polymorphic, and by
 default all universes are hidden from the user. Like implicit