theorem :: ANALORT:23

for V being RealLinearSpace
for u, v, w, x, y being VECTOR of V holds u,v,w,w are_COrtm_wrt x,y by ANALOAF:9;