theorem Th5: :: ANALORT:5

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