let V be RealLinearSpace; :: thesis: for x, y being VECTOR of V st Gen x,y holds
for u, v, w being VECTOR of V ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrte_wrt x,y )
let x, y be VECTOR of V; :: thesis: ( Gen x,y implies for u, v, w being VECTOR of V ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrte_wrt x,y ) )
assume A1: Gen x,y ; :: thesis: for u, v, w being VECTOR of V ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrte_wrt x,y )
let u, v, w be VECTOR of V; :: thesis: ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrte_wrt x,y )

A2: now :: thesis: ( u = v implies ex u1 being M3( the carrier of V) ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrte_wrt x,y ) )

assume A3: u = v ; :: thesis: ex u1 being M3( the carrier of V) ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrte_wrt x,y )
take u1 = w + x; :: thesis: ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrte_wrt x,y )
Orte (x,y,u), Orte (x,y,v) // w,u1 by A3, ANALOAF:9;
then A4: u,v,w,u1 are_COrte_wrt x,y ;

now :: thesis: not w = u1

assume w = u1 ; :: thesis: contradiction
then x = 0. V by RLVECT_1:9;
hence contradiction by A1, Lm4; :: thesis: verum

end;

hence ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrte_wrt x,y ) by A4; :: thesis: verum

end;

now :: thesis: ( u <> v implies ex u1 being M3( the carrier of V) ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrte_wrt x,y ) )

assume A5: u <> v ; :: thesis: ex u1 being M3( the carrier of V) ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrte_wrt x,y )
consider u2 being VECTOR of V such that
A6: Orte (x,y,u2) = u by A1, Th15;
consider v2 being VECTOR of V such that
A7: Orte (x,y,v2) = v by A1, Th15;
take u1 = (u2 + w) - v2; :: thesis: ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrte_wrt x,y )
v2,u2 // w,u1 by ANALOAF:16;
then Orte (x,y,v2), Orte (x,y,u2) // Orte (x,y,w), Orte (x,y,u1) by A1, Th16;
then Orte (x,y,w), Orte (x,y,u1) // v,u by A6, A7, ANALOAF:12;
then Orte (x,y,u1), Orte (x,y,w) // u,v by ANALOAF:12;
then A8: u1,w,u,v are_COrte_wrt x,y ;

now :: thesis: not w = u1

assume w = u1 ; :: thesis: contradiction
then w = w + (u2 - v2) by RLVECT_1:def 3;
then u2 - v2 = 0. V by RLVECT_1:9;
hence contradiction by A5, A6, A7, RLVECT_1:21; :: thesis: verum

end;

hence ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrte_wrt x,y ) by A1, A8, Th18; :: thesis: verum

end;

hence ex u1 being VECTOR of V st
( w <> u1 & u,v,w,u1 are_COrte_wrt x,y ) by A2; :: thesis: verum