theorem Th4: :: ANALORT:4

for V being RealLinearSpace
for u, x, y being VECTOR of V st Gen x,y holds
Ortm (x,y,(- u)) = - (Ortm (x,y,u))