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

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, Def3;
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;

( AS is left_transitive implies 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 )

proof

assume A7: AS is left_transitive ; :: thesis: 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
let v, v1, w, w1, u2, v2 be Element of AS; :: thesis: ( v,v1 // u2,v2 & v,v1 '//' w,w1 & v <> v1 implies u2,v2 '//' w,w1 )
assume that
A8: v,v1 // u2,v2 and
A9: v,v1 '//' w,w1 and
A10: v <> v1 ; :: thesis: u2,v2 '//' w,w1
ex u, u1 being Element of AS st
( u <> u1 & u,u1 '//' v,v1 & u,u1 '//' u2,v2 ) by A8, Def3;
hence u2,v2 '//' w,w1 by A7, A9, A10, Def6; :: thesis: verum

end;

hence ( 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, Def6; :: thesis: verum