:: deftheorem defines are_DTr_wrt GEOMTRAP:def 3 :
for V being RealLinearSpace
for w, y, u, u1, v, v1 being VECTOR of V holds
( u,u1,v,v1 are_DTr_wrt w,y iff ( u,u1 // v,v1 & u,u1,u # u1,v # v1 are_Ort_wrt w,y & v,v1,u # u1,v # v1 are_Ort_wrt w,y ) );