theorem Th7: :: ANALORT:7

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