let AS be Oriented_Orthogonality_Space; ( 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
;
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;
( 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
;
( u = u1 or v = v1 or u2,v2 '//' w,w1 )
now ( u <> u1 & v <> v1 & not u = u1 & not v = v1 implies u2,v2 '//' w,w1 )assume that A6:
u <> u1
and
v <> v1
;
( 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;
verum end;
hence
(
u = u1 or
v = v1 or
u2,
v2 '//' w,
w1 )
;
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; verum