for V being RealLinearSpace
for w, y being VECTOR of V holds w,y are_Ort_wrt w,y