for M being MidSp
for a, b, c, a9, b9, c9 being Element of M st a,b @@ a9,b9 & b,c @@ b9,c9 holds
a,c @@ a9,c9