:: deftheorem Def12 defines ATLAS-like MIDSP_2:def 12 :
for M being non empty MidStr
for IT being AtlasStr over M holds
( IT is ATLAS-like iff ( the algebra of IT is midpoint_operator & the algebra of IT is add-associative & the algebra of IT is right_zeroed & the algebra of IT is right_complementable & the algebra of IT is Abelian & the function of IT is associating & the function of IT is_atlas_of the carrier of M, the algebra of IT ) );