let V be RealLinearSpace; for u, v, w being VECTOR of V holds
( not u,v // u,w or u,v // v,w or u,w // w,v )
let u, v, w be VECTOR of V; ( not u,v // u,w or u,v // v,w or u,w // w,v )
assume A1:
u,v // u,w
; ( u,v // v,w or u,w // w,v )
now ( u <> v & u <> w & not u,v // v,w implies u,w // w,v )assume
(
u <> v &
u <> w )
;
( u,v // v,w or u,w // w,v )then consider a,
b being
Real such that A2:
a * (v - u) = b * (w - u)
and A3:
0 < a
and A4:
0 < b
by A1;
w - v =
(w - u) + (u - v)
by Th1
.=
(w - u) - (v - u)
by RLVECT_1:33
;
then A5:
a * (w - v) =
(a * (w - u)) - (b * (w - u))
by A2, RLVECT_1:34
.=
(a - b) * (w - u)
by RLVECT_1:35
.=
(b - a) * (u - w)
by Th4
;
v - w =
(v - u) + (u - w)
by Th1
.=
(v - u) - (w - u)
by RLVECT_1:33
;
then A6:
b * (v - w) =
(b * (v - u)) - (a * (v - u))
by A2, RLVECT_1:34
.=
(b - a) * (v - u)
by RLVECT_1:35
.=
(a - b) * (u - v)
by Th4
;
A7:
now ( not a <> b or u,v // v,w or u,w // w,v )assume
a <> b
;
( u,v // v,w or u,w // w,v )then
(
0 < a - b or
0 < b - a )
by XREAL_1:55;
then
(
v,
u // w,
v or
w,
u // v,
w )
by A3, A4, A6, A5;
hence
(
u,
v // v,
w or
u,
w // w,
v )
by Th12;
verum end; now ( not a = b or u,v // v,w or u,w // w,v )assume
a = b
;
( u,v // v,w or u,w // w,v )then
(- u) + v = (- u) + w
by A2, A3, RLVECT_1:36;
then
v = w
by RLVECT_1:8;
hence
(
u,
v // v,
w or
u,
w // w,
v )
;
verum end; hence
(
u,
v // v,
w or
u,
w // w,
v )
by A7;
verum end;
hence
( u,v // v,w or u,w // w,v )
; verum