theorem :: ANALORT:22

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