let V be RealLinearSpace; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( 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 ;
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 ; :: thesis: 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 ;
A12: u1,w // Orte (x,y,u1), Orte (x,y,w1) by ;
A13: u1 <> w by ;
A14: not v,u // u1,w by ;
A15: not v,u // w,u1 by ;
( 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 )
proof
assume A16: Gen x,y ; :: thesis: 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

take x ; :: thesis: ex v being VECTOR of V st
for w being VECTOR of V ex a, b being Real st (a * x) + (b * v) = w

take y ; :: thesis: for w being VECTOR of V ex a, b being Real st (a * x) + (b * y) = w
thus for w being VECTOR of V ex a, b being Real st (a * x) + (b * y) = w by ; :: thesis: verum
end;
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 ;
( Orte (x,y,v), Orte (x,y,v1) // v,u2 or Orte (x,y,v), Orte (x,y,v1) // u2,v ) by ;
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 ;
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; :: thesis: verum