Property 4: grantLoyaltyPoints is called only through grantPoints.

That is, within all purse methods $m$ accessible from outside the card, the method $\mathit{L.grantLoyaltyPoints}$ of a loyalty applet $L$ is called only through a call to $\mathit{L'.grantPoints}$ of another loyalty applet $L'$ and never directly by the purse applet.

$$\begin{array}{l} \phi_{4.1} \;\stackrel {\Delta}{=}\; \\ \... ...athsf{through}\\ \qquad loyaltyA.grantPoints \\ \end{array}$$