theorem Th10: :: AFF_2:10
for AP being AffinPlane holds
( AP is satisfying_PPAP iff ( AP is Pappian & AP is satisfying_pap ) )