theorem Th17: :: GEOMTRAP:17

for V being RealLinearSpace
for u, v, w, y being VECTOR of V st u,v,v,u are_DTr_wrt w,y holds
u = v by ANALOAF:10;