:: deftheorem Def5 defines midpoint_operator MIDSP_2:def 5 :
for IT being non empty addLoopStr holds
( IT is midpoint_operator iff ( ( for a being Element of IT ex x being Element of IT st Double x = a ) & ( for a being Element of IT st Double a = 0. IT holds
a = 0. IT ) ) );