apply IsDeduct.axiom_
case h1.a
P S : Formula
⊢ IsDeduct (∅ ∪ {S.imp_ P}) ((P.not_.imp_ (S.not_.imp_ P).not_).imp_ ((S.not_.imp_ P).imp_ P))
case h1.a.a
P S : Formula
⊢ IsAxiom ((P.not_.imp_ (S.not_.imp_ P).not_).imp_ ((S.not_.imp_ P).imp_ P))