for V being RealLinearSpace
for u, u1, v, v1, w, y being VECTOR of V holds
( [[u,v],[u1,v1]] in DTrapezium (V,w,y) iff u,v,u1,v1 are_DTr_wrt w,y )