theorem :: AFF_2:1

for AP being AffinPlane holds
( AP is Pappian iff AP is satisfying_PAP_1 )