theorem :: SCMFSA_X:34

for I being MacroInstruction of SCM+FSA holds stop (Directed I) = I ";" (Stop SCM+FSA) ;