theorem :: AFF_2:1
for AP being AffinPlane holds
( AP is Pappian iff AP is satisfying_PAP_1 )