theorem Th11: :: EUCLMETR:11

for MS being OrtAfPl holds
( MS is Desarguesian iff MS is satisfying_DES ) by Lm2;