theorem :: GEOMTRAP:16

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