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

assume A1: 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 )
A2: ( AS is left_transitive implies AS is right_transitive ) by Th17;
then A3: ( u,u1 '//' v,v1 & v,v1 '//' w1,w & u2,v2 '//' w1,w & u,u1 '//' v,v1 & w,w1 '//' v,v1 & w,w1 '//' u2,v2 & not w = w1 & not v = v1 implies u,u1 '//' u2,v2 ) by A1, Def5, Def6;
assume that
A4: u,u1 '//' v,v1 and
A5: w,w1 '//' v,v1 and
A6: w,w1 '//' u2,v2 ; :: thesis: ( w = w1 or v = v1 or u,u1 '//' u2,v2 )
A7: ( ( 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

A8: now

assume that
A9: u,u1 '//' v2,u2 and
A10: u <> u1 and
A11: v <> v1 and
w <> w1 ; :: thesis: ( ( 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 )

A12: now

assume A13: u2,v2 '//' u,u1 ; :: thesis: ( ( 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 )
then A14: u2,v2 '//' w,w1 by A2, A1, A4, A5, A10, A11, Def5, Def6;

A15: now

assume u2,v2 '//' w1,w ; :: thesis: ( ( 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 )
then ( w = w1 or u2 = v2 ) by A14, Def1;
hence ( ( 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 ) ; :: thesis: verum

end;

w1,w '//' v2,u2 by A6, Def1;
then ( u2,v2 '//' w1,w or u2 = v2 ) by A2, A1, A9, A10, A13, Def5, Def6;
hence ( ( 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 ) by A15; :: thesis: verum

end;

A16: now

A17: w1,w '//' v1,v by A5, Def1;
assume A18: u2,v2 '//' u1,u ; :: thesis: ( ( 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 )
u1,u '//' v1,v by A4, Def1;
then A19: u2,v2 '//' w1,w by A2, A1, A10, A11, A18, A17, Def5, Def6;

A20: now

assume u2,v2 '//' w,w1 ; :: thesis: ( ( 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 )
then ( w = w1 or u2 = v2 ) by A19, Def1;
hence ( ( 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 ) ; :: thesis: verum

end;

u1,u '//' u2,v2 by A9, Def1;
then ( u2,v2 '//' w,w1 or u2 = v2 ) by A2, A1, A6, A10, A18, Def5, Def6;
hence ( ( 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 ) by A20; :: thesis: verum

end;

( v2,u2 '//' u,u1 or v2,u2 '//' u1,u ) by A9, Def1;
hence ( ( 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 ) by A16, A12, Def1; :: thesis: verum

end;

assume ( 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 )
hence ( w = w1 or v = v1 or u,u1 '//' u2,v2 ) by A8, Def1; :: thesis: verum

end;

A21: now

assume that
A22: u,u1 '//' v,v1 and
A23: v,v1 '//' w,w1 and
A24: u2,v2 '//' w1,w ; :: thesis: ( w = w1 or v = v1 or u,u1 '//' u2,v2 )
v2,u2 '//' w,w1 by A24, Def1;
hence ( w = w1 or v = v1 or u,u1 '//' u2,v2 ) by A2, A1, A7, A22, A23, Def5, Def6; :: thesis: verum

end;

A25: now

assume that
A26: u,u1 '//' v,v1 and
A27: v,v1 '//' w1,w and
A28: u2,v2 '//' w,w1 ; :: thesis: ( w = w1 or v = v1 or u,u1 '//' u2,v2 )
v2,u2 '//' w1,w by A28, Def1;
hence ( w = w1 or v = v1 or u,u1 '//' u2,v2 ) by A2, A1, A7, A26, A27, Def5, Def6; :: thesis: verum

end;

( u,u1 '//' v,v1 & v,v1 '//' w,w1 & u2,v2 '//' w,w1 & not w = w1 & not v = v1 implies u,u1 '//' u2,v2 ) by A2, A1, Def5, Def6;
hence ( w = w1 or v = v1 or u,u1 '//' u2,v2 ) by A4, A5, A6, A21, A3, A25, Def1; :: thesis: verum

end;

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