theorem :: ANALORT:21

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