theorem Th32: :: GEOMTRAP:32

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