let V be RealLinearSpace; for p, q, u, v, w, y being VECTOR of V st p <> q & p,q // u,v & p,q // w,y holds
u,v // w,y
let p, q, u, v, w, y be VECTOR of V; ( p <> q & p,q // u,v & p,q // w,y implies u,v // w,y )
assume that
A1:
p <> q
and
A2:
p,q // u,v
and
A3:
p,q // w,y
; u,v // w,y
now ( u <> v & w <> y implies u,v // w,y )assume that A4:
u <> v
and A5:
w <> y
;
u,v // w,yconsider a,
b being
Real such that A6:
a * (q - p) = b * (v - u)
and A7:
0 < a
and A8:
0 < b
by A1, A2, A4;
0 < a "
by A7;
then A9:
0 < (a ") * b
by A8, XREAL_1:129;
consider c,
d being
Real such that A10:
c * (q - p) = d * (y - w)
and A11:
0 < c
and A12:
0 < d
by A1, A3, A5;
A13:
q - p =
(c ") * (d * (y - w))
by A10, A11, Th6
.=
((c ") * d) * (y - w)
by RLVECT_1:def 7
;
0 < c "
by A11;
then A14:
0 < (c ") * d
by A12, XREAL_1:129;
q - p =
(a ") * (b * (v - u))
by A6, A7, Th6
.=
((a ") * b) * (v - u)
by RLVECT_1:def 7
;
hence
u,
v // w,
y
by A13, A9, A14;
verum end;
hence
u,v // w,y
; verum