diff --git a/Concurrent Systems/notes/15 - A formal language for LTSs.md b/Concurrent Systems/notes/15 - A formal language for LTSs.md
index d9abe4a..c1d2c4e 100644
--- a/Concurrent Systems/notes/15 - A formal language for LTSs.md	
+++ b/Concurrent Systems/notes/15 - A formal language for LTSs.md	
@@ -48,4 +48,9 @@ To simplify the proof, let us modify the set of formulae by allowing conjunction
 
 (<=) We prove that $$R \triangleq \{ (P, Q) : L(P)=L(Q) \}$$ is a simulation; this suffices, since the relation just defined is trivially symmetric (so is a bisimulation too).
 
-Let $(P, Q) \in R$ and $$
\ No newline at end of file
+Let $(P, Q) \in R$ and $P \xrightarrow{a} P'$. Let's consider $$\phi \triangleq \phi' \space where \space \phi'\triangleq \bigwedge_{\phi'' \in L(P')}\phi''$$
+By construction, $P \models \phi$, hence, $Q \models \phi$, because $L(Q) = L(P)$; then, $\exists Q' : Q \xrightarrow{a} Q'$ such that $Q'\models \phi'$.
+
+Hence, $\forall \phi'' \in L(P').\phi'' \in L(Q'), \space i.e. \space L(P') \subseteq L(Q')$
+
+By contradiction, let us assume that the inclusion is a proper, i.e. $L(P') \subset L(Q')$.
\ No newline at end of file