 Here it is assumed that \(\TRL(t)=c_2\) for all \(t\) on \(c_2\) after \(t_2\) and that \(\TRL(t)=c_3\) for all \(t\) on \(c_3\) after \(t_2\). Clearly, this means that \(C(t_2)=\{c_2,c_3\}\). In consequence, the proposition \(\Diamond F(y)p\) holds at \(t_2\). This means that \(F(x)\Diamond F(y)p\) is true at \(t_1\). However, the proposition \(\Diamond F(x)F(y)p\) is false at \(t_1\), since \(c_2\) is not included in \(C(t_1)\). According to the definition, \(C(t_1)\) should include exactly the chronicles which pass through \(t_1\) and which immediately after \(t_1\) are specified by the TRL-function. This means that \(C(t_1)=\{c_1,c_3\}\), and then (T5) turns out to be false at \(t_1\).