:: deftheorem defines Stop COMPOS_1:def 16 :
for S being COM-Struct holds Stop S = Load ;