let MS be OrtAfPl; :: thesis: ( MS is Pappian iff MS is satisfying_PAP )
set AS = Af MS;

A1: now

assume MS is satisfying_PAP ; :: thesis: MS is Pappian
then Af MS is Pappian by Lm1;
hence MS is Pappian by Def2; :: thesis: verum

end;

now

assume MS is Pappian ; :: thesis: MS is satisfying_PAP
then Af MS is Pappian by Def2;
hence MS is satisfying_PAP by Lm1; :: thesis: verum

end;

hence ( MS is Pappian iff MS is satisfying_PAP ) by A1; :: thesis: verum