From Believing Modus Ponens and the Rationality Rule we now obtain:

If part of a message is fresh, the whole of the message must be fresh as
well:

Note that the reverse does not hold, since a message can contain ``old
news'' next to new data; the combination is fresh, but every element is
not.

**Proof**

It suffices to prove that all axioms of the BAN logic are theorems of our logic.

is our axiom **Seeing parts of a joint message**, and therefore a
theorem.

both follow from Lemma 4
using the identification of the joining operator on formulas
with the logical-and operator.

follows from the symmetry of the operator.

follows from our axiom
**Saying parts of a joint message**
and Lemma 3.

follows from our axioms
**Possessing believed keys** and **Decryption**.

follows from our axiom
**Awareness**
and Lemmas 3 and 4.

follows from the definition of ,the idempotence of ,and Lemmas 3 and 4.

follows from the definitions of and and Lemmas 3 and 4.