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_COrtm_wrt x,y & not v,v1,u1,w are_COrtm_wrt x,y & u1,w1,u1,w are_COrtm_wrt x,y holds
ex u2 being VECTOR of V st
( ( v,v1,v,u2 are_COrtm_wrt x,y or v,v1,u2,v are_COrtm_wrt x,y ) & ( u1,w1,u1,u2 are_COrtm_wrt x,y or u1,w1,u2,u1 are_COrtm_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_COrtm_wrt x,y & not v,v1,u1,w are_COrtm_wrt x,y & u1,w1,u1,w are_COrtm_wrt x,y holds
ex u2 being VECTOR of V st
( ( v,v1,v,u2 are_COrtm_wrt x,y or v,v1,u2,v are_COrtm_wrt x,y ) & ( u1,w1,u1,u2 are_COrtm_wrt x,y or u1,w1,u2,u1 are_COrtm_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_COrtm_wrt x,y & not v,v1,u1,w are_COrtm_wrt x,y & u1,w1,u1,w are_COrtm_wrt x,y holds
ex u2 being VECTOR of V st
( ( v,v1,v,u2 are_COrtm_wrt x,y or v,v1,u2,v are_COrtm_wrt x,y ) & ( u1,w1,u1,u2 are_COrtm_wrt x,y or u1,w1,u2,u1 are_COrtm_wrt x,y ) )
let v, w, u1, v1, w1 be VECTOR of V; :: thesis: ( not v,v1,w,u1 are_COrtm_wrt x,y & not v,v1,u1,w are_COrtm_wrt x,y & u1,w1,u1,w are_COrtm_wrt x,y implies ex u2 being VECTOR of V st
( ( v,v1,v,u2 are_COrtm_wrt x,y or v,v1,u2,v are_COrtm_wrt x,y ) & ( u1,w1,u1,u2 are_COrtm_wrt x,y or u1,w1,u2,u1 are_COrtm_wrt x,y ) ) )
consider u being VECTOR of V such that
A2: v <> u and
X: v,v1,v,u are_COrtm_wrt x,y by A1, Th41;
assume ( not v,v1,w,u1 are_COrtm_wrt x,y & not v,v1,u1,w are_COrtm_wrt x,y & u1,w1,u1,w are_COrtm_wrt x,y ) ; :: thesis: ex u2 being VECTOR of V st
( ( v,v1,v,u2 are_COrtm_wrt x,y or v,v1,u2,v are_COrtm_wrt x,y ) & ( u1,w1,u1,u2 are_COrtm_wrt x,y or u1,w1,u2,u1 are_COrtm_wrt x,y ) )
then A3: ( not Ortm x,y,v, Ortm x,y,v1 // w,u1 & Ortm x,y,v, Ortm x,y,v1 // v,u & Ortm x,y,u1, Ortm x,y,w1 // u1,w & not Ortm x,y,v, Ortm x,y,v1 // u1,w ) by Def4, X;
then A4: ( v,u // Ortm x,y,v, Ortm x,y,v1 & u1,w // Ortm x,y,u1, Ortm x,y,w1 ) by ANALOAF:21;
A5: u1 <> w by A3, ANALOAF:18;
A6: ( not v,u // u1,w & not v,u // w,u1 ) by A2, A3, A4, ANALOAF:20;
( 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 A7: 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 A7, ANALMETR:def 1; :: thesis: verum

end;

then consider u2 being VECTOR of V such that
A8: ( v,u // v,u2 or v,u // u2,v ) and
A9: ( u1,w // u1,u2 or u1,w // u2,u1 ) by A1, A6, ANALOAF:31;
( Ortm x,y,v, Ortm x,y,v1 // v,u2 or Ortm x,y,v, Ortm x,y,v1 // u2,v ) by A2, A4, A8, ANALOAF:20;
then A10: ( v,v1,v,u2 are_COrtm_wrt x,y or v,v1,u2,v are_COrtm_wrt x,y ) by Def4;
( Ortm x,y,u1, Ortm x,y,w1 // u1,u2 or Ortm x,y,u1, Ortm x,y,w1 // u2,u1 ) by A4, A5, A9, ANALOAF:20;
then ( u1,w1,u1,u2 are_COrtm_wrt x,y or u1,w1,u2,u1 are_COrtm_wrt x,y ) by Def4;
hence ex u2 being VECTOR of V st
( ( v,v1,v,u2 are_COrtm_wrt x,y or v,v1,u2,v are_COrtm_wrt x,y ) & ( u1,w1,u1,u2 are_COrtm_wrt x,y or u1,w1,u2,u1 are_COrtm_wrt x,y ) ) by A10; :: thesis: verum