theorem Th8: :: EUCLMETR:8

for MS being OrtAfPl holds
( MS is Euclidean iff MS is satisfying_3H )