theorem Th11: :: GEOMTRAP:11

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