for V being RealLinearSpace
for x, y being VECTOR of V
for AS being Oriented_Orthogonality_Space st Gen x,y & AS = CESpace (V,x,y) holds
( AS is Euclidean_like & AS is left_transitive & AS is right_transitive & AS is bach_transitive )