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

A1: ( AS is left_transitive implies AS is right_transitive ) by Th17;
assume A2: for u, u1, u2, v, v1, v2, w, w1 being Element of AS st u,u1 '//' v,v1 & v,v1 '//' w,w1 & u,u1 '//' u2,v2 & not u = u1 & not v = v1 holds
u2,v2 '//' w,w1 ; :: 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 A3: ( u,u1 '//' v,v1 & w,w1 '//' v,v1 & w,w1 '//' u2,v2 ) ; :: thesis: ( w = w1 or v = v1 or u,u1 '//' u2,v2 )
A4: ( ( not v = v1 & not w = w1 & not u,u1 '//' u2,v2 & not u,u1 '//' v2,u2 ) or w = w1 or v = v1 or u,u1 '//' u2,v2 )

proof

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

now

assume A6: ( u,u1 '//' v2,u2 & u <> u1 & v <> v1 & w <> w1 ) ; :: thesis: ( w = w1 or v = v1 or u,u1 '//' u2,v2 )
then A7: ( v2,u2 '//' u,u1 or v2,u2 '//' u1,u ) by Def1;

A8: now

assume A9: u2,v2 '//' u1,u ; :: thesis: ( w = w1 or v = v1 or u,u1 '//' u2,v2 )
then ( u2,v2 '//' u1,u & u1,u '//' v1,v & w1,w '//' v1,v ) by A3, Def1;
then A10: u2,v2 '//' w1,w by A1, A2, A6, Def5, Def6;
( u2,v2 '//' u1,u & u1,u '//' u2,v2 & w,w1 '//' u2,v2 ) by A3, A6, A9, Def1;
then A11: ( u2,v2 '//' w,w1 or u2 = v2 ) by A1, A2, A6, Def5, Def6;

now

assume u2,v2 '//' w,w1 ; :: thesis: ( w = w1 or v = v1 or u,u1 '//' u2,v2 )
then ( w = w1 or u2 = v2 ) by A10, Def1;
hence ( w = w1 or v = v1 or u,u1 '//' u2,v2 ) by A6; :: thesis: verum

end;

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

end;

now

assume A12: u2,v2 '//' u,u1 ; :: thesis: ( w = w1 or v = v1 or u,u1 '//' u2,v2 )
then A13: u2,v2 '//' w,w1 by A1, A2, A3, A6, Def5, Def6;
( u2,v2 '//' u,u1 & u,u1 '//' v2,u2 & w1,w '//' v2,u2 ) by A3, A6, A12, Def1;
then A14: ( u2,v2 '//' w1,w or u2 = v2 ) by A1, A2, A6, Def5, Def6;

now

assume u2,v2 '//' w1,w ; :: thesis: ( w = w1 or v = v1 or u,u1 '//' u2,v2 )
then ( w = w1 or u2 = v2 ) by A13, Def1;
hence ( w = w1 or v = v1 or u,u1 '//' u2,v2 ) by A6; :: thesis: verum

end;

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

end;

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

end;

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

end;

A15: ( u,u1 '//' v,v1 & v,v1 '//' w,w1 & u2,v2 '//' w,w1 & not w = w1 & not v = v1 implies u,u1 '//' u2,v2 ) by A1, A2, Def5, Def6;

A16: now

assume ( u,u1 '//' v,v1 & v,v1 '//' w,w1 & u2,v2 '//' w1,w ) ; :: thesis: ( w = w1 or v = v1 or u,u1 '//' u2,v2 )
then ( u,u1 '//' v,v1 & v,v1 '//' w,w1 & v2,u2 '//' w,w1 ) by Def1;
hence ( w = w1 or v = v1 or u,u1 '//' u2,v2 ) by A1, A2, A4, Def5, Def6; :: thesis: verum

end;

A17: ( u,u1 '//' v,v1 & v,v1 '//' w1,w & u2,v2 '//' w1,w & not w = w1 & not v = v1 implies u,u1 '//' u2,v2 ) by A1, A2, Def5, Def6;

now

assume ( u,u1 '//' v,v1 & v,v1 '//' w1,w & u2,v2 '//' w,w1 ) ; :: thesis: ( w = w1 or v = v1 or u,u1 '//' u2,v2 )
then ( u,u1 '//' v,v1 & v,v1 '//' w1,w & v2,u2 '//' w1,w ) by Def1;
hence ( w = w1 or v = v1 or u,u1 '//' u2,v2 ) by A1, A2, A4, Def5, Def6; :: thesis: verum

end;

hence ( w = w1 or v = v1 or u,u1 '//' u2,v2 ) by A3, A15, A16, A17, Def1; :: thesis: verum

end;

hence ( AS is left_transitive implies AS is bach_transitive ) by Def4, Def6; :: thesis: verum