theorem Th8: :: GEOMTRAP:8

for V being RealLinearSpace
for u, v, y being VECTOR of V holds u,v // y # u,y # v