let V be RealLinearSpace; for u, v, w, y being VECTOR of V st u,v // w,y holds
( v,u // y,w & w,y // u,v )
let u, v, w, y be VECTOR of V; ( u,v // w,y implies ( v,u // y,w & w,y // u,v ) )
assume A1:
u,v // w,y
; ( v,u // y,w & w,y // u,v )
now ( u <> v & w <> y implies ( v,u // y,w & w,y // u,v ) )assume
(
u <> v &
w <> y )
;
( v,u // y,w & w,y // u,v )then consider a,
b being
Real such that A2:
a * (v - u) = b * (y - w)
and A3:
(
0 < a &
0 < b )
by A1;
a * (u - v) =
- (b * (y - w))
by A2, Th3
.=
b * (w - y)
by Th3
;
hence
(
v,
u // y,
w &
w,
y // u,
v )
by A2, A3;
verum end;
hence
( v,u // y,w & w,y // u,v )
; verum