consider V being RealLinearSpace, x, y being VECTOR of V such that

A1: Gen x,y by ANALMETR:3;

reconsider AS = CMSpace (V,x,y) as Oriented_Orthogonality_Space by A1, Th3;

take AS ; :: thesis: ( AS is Minkowskian_like & AS is left_transitive & AS is right_transitive & AS is bach_transitive )

thus ( AS is Minkowskian_like & AS is left_transitive & AS is right_transitive & AS is bach_transitive ) by A1, Th14; :: thesis: verum

A1: Gen x,y by ANALMETR:3;

reconsider AS = CMSpace (V,x,y) as Oriented_Orthogonality_Space by A1, Th3;

take AS ; :: thesis: ( AS is Minkowskian_like & AS is left_transitive & AS is right_transitive & AS is bach_transitive )

thus ( AS is Minkowskian_like & AS is left_transitive & AS is right_transitive & AS is bach_transitive ) by A1, Th14; :: thesis: verum