theorem :: GEOMTRAP:15

for V being RealLinearSpace
for u, v, w, y being VECTOR of V st Gen w,y holds
u,u,v,v are_DTr_wrt w,y by Lm5, Lm6, ANALOAF:9;