theorem :: CONMETR1:11

for X being AffinPlane holds
( X is satisfying_PPAP iff X is satisfying_indirect_Scherungssatz )