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

now

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

end;

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