theorem Th40: :: GEOMTRAP:40

for V being RealLinearSpace
for w, y being VECTOR of V st Gen w,y holds
for u, u9, u1, u2, v1, v2, t1, t2, w1, w2 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 & u,u9,v1,w1 are_DTr_wrt w,y & u,u9,v2,w2 are_DTr_wrt w,y & u1,u2,v1,v2 are_Ort_wrt w,y holds
t1,t2,w1,w2 are_Ort_wrt w,y