theorem Th9: :: AFF_2:9

for AP being AffinPlane st AP is Pappian holds
AP is satisfying_pap