theorem Th39: :: GEOMTRAP:39

for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y holds
for u, u9, u1, u2, t1, t2 being VECTOR of V st u <> u9 & u,u9,u1,t1 are_DTr_wrt w,y & u,u9,u2,t2 are_DTr_wrt w,y holds
u,u9,u1 # u2,t1 # t2 are_DTr_wrt w,y