consider M being MidSp;
set G = vectgroup M;
( ( for a being Element of (vectgroup M) ex x being Element of (vectgroup M) st Double x = a ) & ( for a being Element of (vectgroup M) st Double a = 0. (vectgroup M) holds
a = 0. (vectgroup M) ) ) by Lm1;
then vectgroup M is midpoint_operator by Def5;
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