set G = Trivial-addLoopStr ;
A1: for a being Element of Trivial-addLoopStr ex x being Element of Trivial-addLoopStr st Double x = a

proof

consider x being Element of Trivial-addLoopStr ;
let a be Element of Trivial-addLoopStr ; :: thesis: ex x being Element of Trivial-addLoopStr st Double x = a
take x ; :: thesis: Double x = a
thus Double x = {} by CARD_1:87, TARSKI:def 1
.= a by CARD_1:87, TARSKI:def 1 ; :: thesis: verum

end;

for a being Element of Trivial-addLoopStr st Double a = 0. Trivial-addLoopStr holds
a = 0. Trivial-addLoopStr by CARD_1:87, TARSKI:def 1;
hence Trivial-addLoopStr is midpoint_operator by A1, MIDSP_2:def 5; :: thesis: verum