theorem Th10: :: EUCLMETR:10

for MS being OrtAfPl holds
( MS is Pappian iff MS is satisfying_PAP ) by Lm1;