:: deftheorem defines CESpace ANALORT:def 7 :
for V being RealLinearSpace
for x, y being VECTOR of V holds CESpace (V,x,y) = OrtStr(# the carrier of V,(CORTE (V,x,y)) #);