theorem Th14: :: ANALORT:14

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