The hardness proof is trivial, as S5 includes the propositional logic.
难度证明是平凡的，因为 S5 包括命题逻辑。