theorem Th8: :: EUCLMETR:8
for MS being OrtAfPl holds
( MS is Euclidean iff MS is satisfying_3H )