:: deftheorem defines @ MIDSP_1:def 1 :
for MS being non empty MidStr
for a, b being Element of MS holds a @ b = the MIDPOINT of MS . (a,b);