for V being RealLinearSpace
for x, y being VECTOR of V st Gen x,y holds
CESpace (V,x,y) is Oriented_Orthogonality_Space