let AS be Oriented_Orthogonality_Space; :: thesis: ( AS is right_transitive & ( AS is Euclidean_like or AS is Minkowskian_like ) implies AS is left_transitive )
assume A1: AS is right_transitive ; :: thesis: ( ( not AS is Euclidean_like & not AS is Minkowskian_like ) or AS is left_transitive )
( ( for u, u1, v, v1 being Element of AS holds
not ( u,u1 '//' v,v1 & not v,v1 '//' u,u1 & ex u, u1, v, v1 being Element of AS st
( u,u1 '//' v,v1 & not v,v1 '//' u1,u ) ) ) implies 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 )

proof

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

A6: now :: thesis: ( ( for u, u1, v, v1 being Element of AS st u,u1 '//' v,v1 holds
v,v1 '//' u1,u ) & not u = u1 & not v = v1 implies u2,v2 '//' w,w1 )

assume A7: for u, u1, v, v1 being Element of AS st u,u1 '//' v,v1 holds
v,v1 '//' u1,u ; :: thesis: ( u = u1 or v = v1 or u2,v2 '//' w,w1 )

now :: thesis: ( u <> u1 & v <> v1 & not u = u1 & not v = v1 implies u2,v2 '//' w,w1 )

w,w1 '//' v1,v by A4, A7;
then A8: w1,w '//' v,v1 by Def1;
A9: u2,v2 '//' u1,u by A5, A7;
assume that
A10: u <> u1 and
A11: v <> v1 ; :: thesis: ( u = u1 or v = v1 or u2,v2 '//' w,w1 )
v,v1 '//' u1,u by A3, A7;
then w1,w '//' u2,v2 by A1, A10, A11, A8, A9;
hence ( u = u1 or v = v1 or u2,v2 '//' w,w1 ) by A7; :: thesis: verum

end;

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

end;

now :: thesis: ( ( for u, u1, v, v1 being Element of AS st u,u1 '//' v,v1 holds
v,v1 '//' u,u1 ) & not u = u1 & not v = v1 implies u2,v2 '//' w,w1 )

assume A12: for u, u1, v, v1 being Element of AS st u,u1 '//' v,v1 holds
v,v1 '//' u,u1 ; :: thesis: ( u = u1 or v = v1 or u2,v2 '//' w,w1 )

now :: thesis: ( u <> u1 & v <> v1 & not u = u1 & not v = v1 implies u2,v2 '//' w,w1 )

A13: u2,v2 '//' u,u1 by A5, A12;
A14: w,w1 '//' v,v1 by A4, A12;
assume that
A15: u <> u1 and
A16: v <> v1 ; :: thesis: ( u = u1 or v = v1 or u2,v2 '//' w,w1 )
v,v1 '//' u,u1 by A3, A12;
then w,w1 '//' u2,v2 by A1, A15, A16, A14, A13;
hence ( u = u1 or v = v1 or u2,v2 '//' w,w1 ) by A12; :: thesis: verum

end;

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

end;

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

end;

hence ( ( not AS is Euclidean_like & not AS is Minkowskian_like ) or AS is left_transitive ) ; :: thesis: verum