for V being RealLinearSpace
for x, y being VECTOR of V st Gen x,y holds
for v, w, u1, v1, w1 being VECTOR of V st not v,v1,w,u1 are_COrte_wrt x,y & not v,v1,u1,w are_COrte_wrt x,y & u1,w1,u1,w are_COrte_wrt x,y holds
ex u2 being VECTOR of V st
( ( v,v1,v,u2 are_COrte_wrt x,y or v,v1,u2,v are_COrte_wrt x,y ) & ( u1,w1,u1,u2 are_COrte_wrt x,y or u1,w1,u2,u1 are_COrte_wrt x,y ) )