:: deftheorem Def8 defines MidPoint GEOMTRAP:def 8 :
for V being RealLinearSpace
for b₂ being BinOp of the carrier of V holds
( b₂ = MidPoint V iff for u, v being VECTOR of V holds b₂ . (u,v) = u # v );