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