for V being RealLinearSpace
for u, u1, v, v1, x, y being VECTOR of V st Gen x,y & u,v // u1,v1 holds
Ortm (x,y,u), Ortm (x,y,v) // Ortm (x,y,u1), Ortm (x,y,v1)