let AS be Oriented_Orthogonality_Space; :: thesis: ( AS is bach_transitive implies for u, u1, v, v1, w, w1 being Element of AS st u,u1 // v,v1 & v,v1 // w,w1 & v <> v1 holds
u,u1 // w,w1 )
assume A1: AS is bach_transitive ; :: thesis: for u, u1, v, v1, w, w1 being Element of AS st u,u1 // v,v1 & v,v1 // w,w1 & v <> v1 holds
u,u1 // w,w1
let u, u1, v, v1, w, w1 be Element of AS; :: thesis: ( u,u1 // v,v1 & v,v1 // w,w1 & v <> v1 implies u,u1 // w,w1 )
assume that
A2: u,u1 // v,v1 and
A3: v,v1 // w,w1 and
A4: v <> v1 ; :: thesis: u,u1 // w,w1
consider v2, v3 being Element of AS such that
A5: v2 <> v3 and
A6: v2,v3 '//' u,u1 and
A7: v2,v3 '//' v,v1 by A2;
v2,v3 '//' w,w1 by A1, A3, A4, A7;
hence u,u1 // w,w1 by A5, A6; :: thesis: verum