let V be RealLinearSpace; :: thesis: for x, y, u, u1, v, v1 being VECTOR of V st Gen x,y & u,u1,v,v1 are_COrte_wrt x,y holds
v,v1,u1,u are_COrte_wrt x,y
let x, y, u, u1, v, v1 be VECTOR of V; :: thesis: ( Gen x,y & u,u1,v,v1 are_COrte_wrt x,y implies v,v1,u1,u are_COrte_wrt x,y )
assume A1: Gen x,y ; :: thesis: ( not u,u1,v,v1 are_COrte_wrt x,y or v,v1,u1,u are_COrte_wrt x,y )
assume u,u1,v,v1 are_COrte_wrt x,y ; :: thesis: v,v1,u1,u are_COrte_wrt x,y
then Orte x,y,u, Orte x,y,u1 // v,v1 by Def3;
then v,v1 // Orte x,y,u, Orte x,y,u1 by ANALOAF:21;
then Orte x,y,v, Orte x,y,v1 // Orte x,y,(Orte x,y,u), Orte x,y,(Orte x,y,u1) by A1, Th16;
then Orte x,y,v, Orte x,y,v1 // - u, Orte x,y,(Orte x,y,u1) by A1, Th14;
then Orte x,y,v, Orte x,y,v1 // - u, - u1 by A1, Th14;
then A2: - u, - u1 // Orte x,y,v, Orte x,y,v1 by ANALOAF:21;
(- u1) - (- u) = u + (- u1) by RLVECT_1:30
.= u - u1 ;
then A3: - u, - u1 // u1,u by ANALOAF:24;

A4: now

assume - u <> - u1 ; :: thesis: v,v1,u1,u are_COrte_wrt x,y
then Orte x,y,v, Orte x,y,v1 // u1,u by A2, A3, ANALOAF:20;
hence v,v1,u1,u are_COrte_wrt x,y by Def3; :: thesis: verum

end;

now

assume - u = - u1 ; :: thesis: v,v1,u1,u are_COrte_wrt x,y
then u = - (- u1) by RLVECT_1:30
.= u1 by RLVECT_1:30 ;
then Orte x,y,v, Orte x,y,v1 // u1,u by ANALOAF:18;
hence v,v1,u1,u are_COrte_wrt x,y by Def3; :: thesis: verum

end;

hence v,v1,u1,u are_COrte_wrt x,y by A4; :: thesis: verum