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

now :: thesis: ( u <> v & not u,v,v1,w are_COrte_wrt x,y implies u,v,w,v1 are_COrte_wrt x,y )

assume A6: u <> v ; :: thesis: ( u,v,v1,w are_COrte_wrt x,y or u,v,w,v1 are_COrte_wrt x,y )

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

assume that
A7: u1 <> v1 and
A8: u1 <> w ; :: thesis: ( u,v,v1,w are_COrte_wrt x,y or u,v,w,v1 are_COrte_wrt x,y )
A9: u1,v1 // u1,w by A1, A4, A5, A6, Th13, ANALOAF:11;

A10: now :: thesis: ( u1,v1 // v1,w & not u,v,v1,w are_COrte_wrt x,y implies u,v,w,v1 are_COrte_wrt x,y )

assume A11: u1,v1 // v1,w ; :: thesis: ( u,v,v1,w are_COrte_wrt x,y or u,v,w,v1 are_COrte_wrt x,y )
u1,v1 // Orte (x,y,u), Orte (x,y,v) by A4, ANALOAF:12;
then Orte (x,y,u), Orte (x,y,v) // v1,w by A7, A11, ANALOAF:11;
hence ( u,v,v1,w are_COrte_wrt x,y or u,v,w,v1 are_COrte_wrt x,y ) ; :: thesis: verum

end;

now :: thesis: ( u1,w // w,v1 & not u,v,v1,w are_COrte_wrt x,y implies u,v,w,v1 are_COrte_wrt x,y )

assume A12: u1,w // w,v1 ; :: thesis: ( u,v,v1,w are_COrte_wrt x,y or u,v,w,v1 are_COrte_wrt x,y )
u1,w // Orte (x,y,u), Orte (x,y,v) by A5, ANALOAF:12;
then Orte (x,y,u), Orte (x,y,v) // w,v1 by A8, A12, ANALOAF:11;
hence ( u,v,v1,w are_COrte_wrt x,y or u,v,w,v1 are_COrte_wrt x,y ) ; :: thesis: verum

end;

hence ( u,v,v1,w are_COrte_wrt x,y or u,v,w,v1 are_COrte_wrt x,y ) by A9, A10, ANALOAF:14; :: thesis: verum

end;

hence ( u,v,v1,w are_COrte_wrt x,y or u,v,w,v1 are_COrte_wrt x,y ) by A2, A3; :: thesis: verum

end;

hence ( u,v,v1,w are_COrte_wrt x,y or u,v,w,v1 are_COrte_wrt x,y ) by Th20; :: thesis: verum