let V be RealLinearSpace; for x, y being VECTOR of V st Gen x,y holds
for v, w, u1, v1, w1 being VECTOR of V st not v,v1,w,u1 are_COrte_wrt x,y & not v,v1,u1,w are_COrte_wrt x,y & u1,w1,u1,w are_COrte_wrt x,y holds
ex u2 being VECTOR of V st
( ( v,v1,v,u2 are_COrte_wrt x,y or v,v1,u2,v are_COrte_wrt x,y ) & ( u1,w1,u1,u2 are_COrte_wrt x,y or u1,w1,u2,u1 are_COrte_wrt x,y ) )
let x, y be VECTOR of V; ( Gen x,y implies for v, w, u1, v1, w1 being VECTOR of V st not v,v1,w,u1 are_COrte_wrt x,y & not v,v1,u1,w are_COrte_wrt x,y & u1,w1,u1,w are_COrte_wrt x,y holds
ex u2 being VECTOR of V st
( ( v,v1,v,u2 are_COrte_wrt x,y or v,v1,u2,v are_COrte_wrt x,y ) & ( u1,w1,u1,u2 are_COrte_wrt x,y or u1,w1,u2,u1 are_COrte_wrt x,y ) ) )
assume A1:
Gen x,y
; for v, w, u1, v1, w1 being VECTOR of V st not v,v1,w,u1 are_COrte_wrt x,y & not v,v1,u1,w are_COrte_wrt x,y & u1,w1,u1,w are_COrte_wrt x,y holds
ex u2 being VECTOR of V st
( ( v,v1,v,u2 are_COrte_wrt x,y or v,v1,u2,v are_COrte_wrt x,y ) & ( u1,w1,u1,u2 are_COrte_wrt x,y or u1,w1,u2,u1 are_COrte_wrt x,y ) )
let v, w, u1, v1, w1 be VECTOR of V; ( not v,v1,w,u1 are_COrte_wrt x,y & not v,v1,u1,w are_COrte_wrt x,y & u1,w1,u1,w are_COrte_wrt x,y implies ex u2 being VECTOR of V st
( ( v,v1,v,u2 are_COrte_wrt x,y or v,v1,u2,v are_COrte_wrt x,y ) & ( u1,w1,u1,u2 are_COrte_wrt x,y or u1,w1,u2,u1 are_COrte_wrt x,y ) ) )
consider u being VECTOR of V such that
A2:
v <> u
and
A3:
v,v1,v,u are_COrte_wrt x,y
by A1, Th40;
assume that
A4:
not v,v1,w,u1 are_COrte_wrt x,y
and
A5:
not v,v1,u1,w are_COrte_wrt x,y
and
A6:
u1,w1,u1,w are_COrte_wrt x,y
; ex u2 being VECTOR of V st
( ( v,v1,v,u2 are_COrte_wrt x,y or v,v1,u2,v are_COrte_wrt x,y ) & ( u1,w1,u1,u2 are_COrte_wrt x,y or u1,w1,u2,u1 are_COrte_wrt x,y ) )
A7:
not Orte (x,y,v), Orte (x,y,v1) // w,u1
by A4;
A8:
Orte (x,y,v), Orte (x,y,v1) // v,u
by A3;
A9:
Orte (x,y,u1), Orte (x,y,w1) // u1,w
by A6;
A10:
not Orte (x,y,v), Orte (x,y,v1) // u1,w
by A5;
A11:
v,u // Orte (x,y,v), Orte (x,y,v1)
by A8, ANALOAF:12;
A12:
u1,w // Orte (x,y,u1), Orte (x,y,w1)
by A9, ANALOAF:12;
A13:
u1 <> w
by A7, ANALOAF:9;
A14:
not v,u // u1,w
by A2, A10, A11, ANALOAF:11;
A15:
not v,u // w,u1
by A2, A7, A11, ANALOAF:11;
( Gen x,y implies ex u, v being VECTOR of V st
for w being VECTOR of V ex a, b being Real st (a * u) + (b * v) = w )
then consider u2 being VECTOR of V such that
A17:
( v,u // v,u2 or v,u // u2,v )
and
A18:
( u1,w // u1,u2 or u1,w // u2,u1 )
by A1, A14, A15, ANALOAF:21;
( Orte (x,y,v), Orte (x,y,v1) // v,u2 or Orte (x,y,v), Orte (x,y,v1) // u2,v )
by A2, A11, A17, ANALOAF:11;
then A19:
( v,v1,v,u2 are_COrte_wrt x,y or v,v1,u2,v are_COrte_wrt x,y )
;
( Orte (x,y,u1), Orte (x,y,w1) // u1,u2 or Orte (x,y,u1), Orte (x,y,w1) // u2,u1 )
by A12, A13, A18, ANALOAF:11;
then
( u1,w1,u1,u2 are_COrte_wrt x,y or u1,w1,u2,u1 are_COrte_wrt x,y )
;
hence
ex u2 being VECTOR of V st
( ( v,v1,v,u2 are_COrte_wrt x,y or v,v1,u2,v are_COrte_wrt x,y ) & ( u1,w1,u1,u2 are_COrte_wrt x,y or u1,w1,u2,u1 are_COrte_wrt x,y ) )
by A19; verum