:: deftheorem Def6 defines Half MIDSP_2:def 6 :
for G being non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr
for x, b₃ being Element of G holds
( b₃ = Half x iff Double b₃ = x );