theorem :: COMPOS_1:27

for S being COM-Struct
for F being MacroInstruction of S holds F ';' (Stop S) = F ;