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

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