consider V being RealLinearSpace, x, y being VECTOR of V such that
A1: Gen x,y by ANALMETR:3;
reconsider AS = CESpace (V,x,y) as Oriented_Orthogonality_Space by A1, Th4;
take AS ; :: thesis: ( AS is Euclidean_like & AS is left_transitive & AS is right_transitive & AS is bach_transitive )
thus ( AS is Euclidean_like & AS is left_transitive & AS is right_transitive & AS is bach_transitive ) by A1, Th13; :: thesis: verum