theorem Th33: :: GEOMTRAP:33

for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y holds
for u, v, u1, v1 being VECTOR of V holds
( u,v,u1,v1 are_Ort_wrt w,y iff PProJ (w,y,(v - u),(v1 - u1)) = 0 )