theorem Th11: :: ANALORT:11

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