theorem Th18: :: GEOMTRAP:18

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