theorem Th13: :: GEOMTRAP:13

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