let V be RealLinearSpace; :: thesis: for u, u1, u2, v, v1, v2, w, w1, x, y being VECTOR of V st Gen x,y & u,u1,v,v1 are_COrte_wrt x,y & v,v1,w,w1 are_COrte_wrt x,y & u2,v2,w,w1 are_COrte_wrt x,y & not u,u1,u2,v2 are_COrte_wrt x,y & not v = v1 holds
w = w1
let u, u1, u2, v, v1, v2, w, w1, x, y be VECTOR of V; :: thesis: ( Gen x,y & u,u1,v,v1 are_COrte_wrt x,y & v,v1,w,w1 are_COrte_wrt x,y & u2,v2,w,w1 are_COrte_wrt x,y & not u,u1,u2,v2 are_COrte_wrt x,y & not v = v1 implies w = w1 )
assume A1: Gen x,y ; :: thesis: ( not u,u1,v,v1 are_COrte_wrt x,y or not v,v1,w,w1 are_COrte_wrt x,y or not u2,v2,w,w1 are_COrte_wrt x,y or u,u1,u2,v2 are_COrte_wrt x,y or v = v1 or w = w1 )
assume that
A2: u,u1,v,v1 are_COrte_wrt x,y and
A3: v,v1,w,w1 are_COrte_wrt x,y and
A4: u2,v2,w,w1 are_COrte_wrt x,y ; :: thesis: ( u,u1,u2,v2 are_COrte_wrt x,y or v = v1 or w = w1 )
v,v1,u1,u are_COrte_wrt x,y by A1, A2, Th18;
then A5: Orte (x,y,v), Orte (x,y,v1) // u1,u ;
Orte (x,y,v), Orte (x,y,v1) // w,w1 by A3;
then A6: w,w1 // Orte (x,y,v), Orte (x,y,v1) by ANALOAF:12;
Orte (x,y,u2), Orte (x,y,v2) // w,w1 by A4;
then A7: w,w1 // Orte (x,y,u2), Orte (x,y,v2) by ANALOAF:12;

now :: thesis: ( w <> w1 & v <> v1 & not u,u1,u2,v2 are_COrte_wrt x,y & not v = v1 implies w = w1 )

assume that
A8: w <> w1 and
A9: v <> v1 ; :: thesis: ( u,u1,u2,v2 are_COrte_wrt x,y or v = v1 or w = w1 )
Orte (x,y,v), Orte (x,y,v1) // Orte (x,y,u2), Orte (x,y,v2) by A6, A7, A8, ANALOAF:11;
then Orte (x,y,u2), Orte (x,y,v2) // u1,u by A1, A5, A9, Th13, ANALOAF:11;
then Orte (x,y,v2), Orte (x,y,u2) // u,u1 by ANALOAF:12;
then v2,u2,u,u1 are_COrte_wrt x,y ;
hence ( u,u1,u2,v2 are_COrte_wrt x,y or v = v1 or w = w1 ) by A1, Th18; :: thesis: verum

end;

hence ( u,u1,u2,v2 are_COrte_wrt x,y or v = v1 or w = w1 ) ; :: thesis: verum