theorem :: ANALORT:26

for V being RealLinearSpace
for u, v, x, y being VECTOR of V holds u,v, Ortm (x,y,u), Ortm (x,y,v) are_COrtm_wrt x,y by ANALOAF:8;