for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y holds
for u, v being VECTOR of V st u <> v holds
PProJ (w,y,(u - v),(u - v)) <> 0