theorem :: EUCLMETR:23

for MS being OrtAfPl
for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y & MS = AMSpace (V,w,y) holds
MS is Euclidean Pappian Desarguesian Fanoian Moufangian translation Homogeneous OrtAfPl