:: deftheorem Def7 defines DTrapezium GEOMTRAP:def 7 :
for V being RealLinearSpace
for w, y being VECTOR of V
for b₄ being Relation of [: the carrier of V, the carrier of V:] holds
( b₄ = DTrapezium (V,w,y) iff for x, z being object holds
( [x,z] in b₄ iff ex u, u1, v, v1 being VECTOR of V st
( x = [u,u1] & z = [v,v1] & u,u1,v,v1 are_DTr_wrt w,y ) ) );