theorem :: COMPOS_1:68

for S being COM-Struct
for p being initial preProgram of S holds CutLastLoc (stop p) = p ;