:: deftheorem defines 0. MIDSP_2:def 15 :
for M being MidSp
for W being ATLAS of M holds 0. W = 0. the algebra of W;