set M = the MidSp;
set G = vectgroup the MidSp;
( ( for a being Element of (vectgroup the MidSp) ex x being Element of (vectgroup the MidSp) st Double x = a ) & ( for a being Element of (vectgroup the MidSp) st Double a = 0. (vectgroup the MidSp) holds
a = 0. (vectgroup the MidSp) ) ) by Lm1;
then vectgroup the MidSp is midpoint_operator ;
hence ex b₁ being non empty addLoopStr st
( b₁ is strict & b₁ is midpoint_operator & b₁ is add-associative & b₁ is right_zeroed & b₁ is right_complementable & b₁ is Abelian ) ; :: thesis: verum