diff --git a/DistributedTransaction/README.md b/DistributedTransaction/README.md
index 2a1c680..1d4a4b4 100644
--- a/DistributedTransaction/README.md
+++ b/DistributedTransaction/README.md
@@ -4,7 +4,6 @@ The module contains a abstract specification of the transaction system implement
 
 The module contains two TLA+ files: `DistributedTransaction.tla` and `DistributedTransactionProofs.tla`.
 
-In most cases you will only have an interest in `DistributedTransaction.tla`, where the whole specification and safety invariants are defined. Besides that, in `DistributedTransactionProofs.tla`, there are some proofs, which are supposed to be build up gradually, to the safety invariants.
-
-To run formal proofs in `DistributedTransactionProofs.tla`, you'd better install [TLAPS](https://tla.msr-inria.inria.fr/tlaps/content/Download/Binaries.html) (TLA+ Proof System) first. It's not distributed altogether with the TLA toolbox.
+In most cases you will likely have an interest in only `DistributedTransaction.tla`, where the specification and safety invariants are defined. Besides that, in `DistributedTransactionProofs.tla`, there are some formal proofs, which are supposed to be build up gradually (so it's not completed yet), to the safety invariants.
 
+To run the formal proofs in `DistributedTransactionProofs.tla`, you'd like to install the [TLAPS](https://tla.msr-inria.inria.fr/tlaps/content/Download/Binaries.html) (TLA+ Proof System) first. It's not distributed altogether with the TLA toolbox.