let AS be Oriented_Orthogonality_Space; ( AS is right_transitive & ( AS is Euclidean_like or AS is Minkowskian_like ) implies AS is left_transitive )
assume A1:
AS is right_transitive
; ( ( 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 ) )
;
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 )
A6:
now ( ( 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
;
( 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 )
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
;
( 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;
verum end; hence
(
u = u1 or
v = v1 or
u2,
v2 '//' w,
w1 )
;
verum end;
now ( ( 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
;
( 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 )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
;
( 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;
verum end; hence
(
u = u1 or
v = v1 or
u2,
v2 '//' w,
w1 )
;
verum end;
hence
(
u = u1 or
v = v1 or
u2,
v2 '//' w,
w1 )
by A2, A6;
verum
end;
hence
( ( not AS is Euclidean_like & not AS is Minkowskian_like ) or AS is left_transitive )
; verum