set G = addLoopStr(# 1,op2 ,op0 #);
A1: for a being Element of addLoopStr(# 1,op2 ,op0 #) ex x being Element of addLoopStr(# 1,op2 ,op0 #) st Double x = a

proof

consider x being Element of addLoopStr(# 1,op2 ,op0 #);
let a be Element of addLoopStr(# 1,op2 ,op0 #); :: thesis: ex x being Element of addLoopStr(# 1,op2 ,op0 #) 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 addLoopStr(# 1,op2 ,op0 #) st Double a = 0. addLoopStr(# 1,op2 ,op0 #) holds
a = 0. addLoopStr(# 1,op2 ,op0 #) by CARD_1:87, TARSKI:def 1;
hence addLoopStr(# 1,op2 ,op0 #) is midpoint_operator by A1, MIDSP_2:def 5; :: thesis: verum