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

proof

assume A2: for v, v1, w, w1, u2, v2 being Element of AS st v,v1 // u2,v2 & v,v1 '//' w,w1 & 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 & 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 )

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

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

end;

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

end;

thus ( AS is left_transitive iff for v, v1, w, w1, u2, v2 being Element of AS st v,v1 // u2,v2 & v,v1 '//' w,w1 & v <> v1 holds
u2,v2 '//' w,w1 ) by A1; :: thesis: verum