for V being RealLinearSpace
for u, u1, v, v1, x, y 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