theorem Th9: :: CONMETR1:9

for X being AffinPlane holds
( X is satisfying_pap iff X is satisfying_minor_indirect_Scherungssatz )