for V being RealLinearSpace
for u, u1, v, v1, w, x, y being VECTOR of V st Gen x,y & u,v,u1,v1 are_COrtm_wrt x,y & u,v,v1,w are_COrtm_wrt x,y holds
u,v,u1,w are_COrtm_wrt x,y