for MS being OrtAfPl holds
( MS is Pappian iff MS is satisfying_PAP ) by Lm1;