theorem Th15: :: MIDSP_1:15

for M being MidSp
for a, b, c being Element of M ex d being Element of M st a,b @@ c,d