theorem :: COMPOS_1:28

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