theorem :: ANALORT:43

for V being RealLinearSpace
for u, u1, u2, v, v1, v2, w, w1, x, y being VECTOR of V st Gen x,y & u,u1,v,v1 are_COrtm_wrt x,y & w,w1,v,v1 are_COrtm_wrt x,y & w,w1,u2,v2 are_COrtm_wrt x,y & not w = w1 & not v = v1 holds
u,u1,u2,v2 are_COrtm_wrt x,y