theorem Th25: :: GEOMTRAP:25

for V being RealLinearSpace
for u, u1, v, v1, v2, w, y being VECTOR of V st Gen w,y & u <> u1 & u,u1,v,v1 are_DTr_wrt w,y & ( u,u1,v,v2 are_DTr_wrt w,y or u,u1,v2,v are_DTr_wrt w,y ) holds
v1 = v2