theorem :: EUCLMETR:12

for MS being OrtAfPl holds
( MS is Moufangian iff MS is satisfying_TDES )