theorem :: ANALORT:35

for V being RealLinearSpace
for u, u1, v, v1, x, y being VECTOR of V st u,v,u1,v1 are_COrtm_wrt x,y holds
v,u,v1,u1 are_COrtm_wrt x,y by ANALOAF:12;