:: deftheorem defines DTrSpace GEOMTRAP:def 9 :
for V being RealLinearSpace
for w, y being VECTOR of V holds DTrSpace (V,w,y) = AfMidStruct(# the carrier of V,(MidPoint V),(DTrapezium (V,w,y)) #);