theorem Th10: :: GEOMTRAP:10

for V being RealLinearSpace
for u, v being VECTOR of V holds
( 2 * ((u # v) - u) = v - u & 2 * (v - (u # v)) = v - u )