theorem Th14: :: DIRORT:14

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