:: deftheorem defines stop COMPOS_1:def 24 :
for S being COM-Struct
for I being initial preProgram of S holds stop I = I ^ (Stop S);