  We present the system G3S5, a Gentzen-style sequent calculus system for the
modal propositional logic S5, which in a sense has the subformula property. We
formulate the rules of G3 S5 in the system G3S5; which has the subformula
property and prove the admissibility of the weakening, contraction and cut
rules for it.
