theorem Th15: :: DIRORT:15

for AS being Oriented_Orthogonality_Space st AS is left_transitive holds
AS is right_transitive