:: deftheorem defines CMSpace ANALORT:def 8 :
for V being RealLinearSpace
for x, y being VECTOR of V holds CMSpace (V,x,y) = OrtStr(# the carrier of V,(CORTM (V,x,y)) #);