theorem :: ANALORT:28

for V being RealLinearSpace
for u, u1, v, v1, x, y being VECTOR of V st Gen x,y holds
( u,v // u1,v1 iff ex u2, v2 being VECTOR of V st
( u2 <> v2 & u2,v2,u,v are_COrtm_wrt x,y & u2,v2,u1,v1 are_COrtm_wrt x,y ) )