:: deftheorem Def2 defines # GEOMTRAP:def 2 :
for V being RealLinearSpace
for u, v, b₄ being VECTOR of V holds
( b₄ = u # v iff b₄ + b₄ = u + v );