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