for AS being Oriented_Orthogonality_Space holds
( AS is bach_transitive iff for u, u1, u2, v, v1, v2 being Element of AS st u,u1 '//' v,v1 & v,v1 // u2,v2 & v <> v1 holds
u,u1 '//' u2,v2 )