theorem Th1: :: MIDSP_2:1

for G being non empty addLoopStr
for M being non empty MidStr
for p being Point of M
for w being Function of [: the carrier of M, the carrier of M:], the carrier of G st w is associating holds
p @ p = p