let AS be Oriented_Orthogonality_Space; :: thesis: ( 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 )
A1: ( ( 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 ) implies for u, u1, u2, v, v1, v2, w, w1 being Element of AS st u,u1 '//' v,v1 & w,w1 '//' v,v1 & w,w1 '//' u2,v2 & not w = w1 & not v = v1 holds
u,u1 '//' u2,v2 )

proof

assume A2: 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 ; :: thesis: for u, u1, u2, v, v1, v2, w, w1 being Element of AS st u,u1 '//' v,v1 & w,w1 '//' v,v1 & w,w1 '//' u2,v2 & not w = w1 & not v = v1 holds
u,u1 '//' u2,v2
let u, u1, u2, v, v1, v2, w, w1 be Element of AS; :: thesis: ( u,u1 '//' v,v1 & w,w1 '//' v,v1 & w,w1 '//' u2,v2 & not w = w1 & not v = v1 implies u,u1 '//' u2,v2 )
assume that
A3: u,u1 '//' v,v1 and
A4: w,w1 '//' v,v1 and
A5: w,w1 '//' u2,v2 ; :: thesis: ( w = w1 or v = v1 or u,u1 '//' u2,v2 )

now

assume that
A6: w <> w1 and
v <> v1 ; :: thesis: ( w = w1 or v = v1 or u,u1 '//' u2,v2 )
v,v1 // u2,v2 by A4, A5, A6, Def3;
hence ( w = w1 or v = v1 or u,u1 '//' u2,v2 ) by A2, A3; :: thesis: verum

end;

hence ( w = w1 or v = v1 or u,u1 '//' u2,v2 ) ; :: thesis: verum

end;

( AS is bach_transitive implies 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 )

proof

assume A7: AS is bach_transitive ; :: thesis: 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
let u, u1, u2, v, v1, v2 be Element of AS; :: thesis: ( u,u1 '//' v,v1 & v,v1 // u2,v2 & v <> v1 implies u,u1 '//' u2,v2 )
assume that
A8: u,u1 '//' v,v1 and
A9: v,v1 // u2,v2 and
A10: v <> v1 ; :: thesis: u,u1 '//' u2,v2
ex w, w1 being Element of AS st
( w <> w1 & w,w1 '//' v,v1 & w,w1 '//' u2,v2 ) by A9, Def3;
hence u,u1 '//' u2,v2 by A7, A8, A10, Def4; :: thesis: verum

end;

hence ( 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 ) by A1, Def4; :: thesis: verum