  In the framework of Berthelot's theory of arithmetic $\mathcal{D}$-modules,
we prove that Berthelot's characteristic variety associated with a holonomic
$\mathcal{D}$-modules endowed with a Frobenius structure has pure dimension. As
an application, we get the lagrangianity of the characteristic variety of a log
extendable overconvergent $F$-isocrystal.
