set G = Trivial-addLoopStr ;
A1: for a being Element of Trivial-addLoopStr ex x being Element of Trivial-addLoopStr st Double x = a
proof
set x = the Element of Trivial-addLoopStr;
let a be Element of Trivial-addLoopStr; :: thesis: ex x being Element of Trivial-addLoopStr st Double x = a
take the Element of Trivial-addLoopStr ; :: thesis: Double the Element of Trivial-addLoopStr = a
thus Double the Element of Trivial-addLoopStr = {} by TARSKI:def 1
.= a by 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 TARSKI:def 1;
hence Trivial-addLoopStr is midpoint_operator by A1, MIDSP_2:def 5; :: thesis: verum