:: deftheorem defines AMSpace ANALMETR:def 6 :
for V being RealLinearSpace
for w, y being VECTOR of V holds AMSpace (V,w,y) = ParOrtStr(# the carrier of V,(lambda (DirPar V)),(Orthogonality (V,w,y)) #);