theorem Th12: :: GEOMTRAP:12

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