:: deftheorem defines MidSp. MIDSP_2:def 11 :
for S being non empty set
for G being non empty right_complementable Abelian add-associative right_zeroed midpoint_operator addLoopStr
for w being Function of [:S,S:], the carrier of G st w is_atlas_of S,G holds
MidSp. w = MidStr(# S,(@ w) #);