let V be RealLinearSpace; ( ex p, q being VECTOR of V st p <> q implies for u, v, w being VECTOR of V ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y ) )
given p, q being VECTOR of V such that A1:
p <> q
; for u, v, w being VECTOR of V ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y )
let u, v, w be VECTOR of V; ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y )
A2:
now ( u <> w implies ex y being M3( the carrier of V) ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y ) )assume A3:
u <> w
;
ex y being M3( the carrier of V) ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y )take y =
(v + w) - u;
ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y )
(
u,
v // w,
y &
u,
w // v,
y )
by Th16;
hence
ex
y being
VECTOR of
V st
(
u,
v // w,
y &
u,
w // v,
y &
v <> y )
by A4;
verum end;
now ( u = w implies ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y ) )assume A5:
u = w
;
ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y )A6:
now ( u = v implies ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y ) )assume
u = v
;
ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y )then A7:
(
u,
v // w,
p &
u,
v // w,
q )
;
A8:
(
v <> p or
v <> q )
by A1;
(
u,
w // v,
p &
u,
w // v,
q )
by A5;
hence
ex
y being
VECTOR of
V st
(
u,
v // w,
y &
u,
w // v,
y &
v <> y )
by A8, A7;
verum end;
(
u,
v // w,
u &
u,
w // v,
u )
by A5;
hence
ex
y being
VECTOR of
V st
(
u,
v // w,
y &
u,
w // v,
y &
v <> y )
by A6;
verum end;
hence
ex y being VECTOR of V st
( u,v // w,y & u,w // v,y & v <> y )
by A2; verum