theorem Th9: :: ANALORT:9

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