theorem Th4: :: SCMPDS_7:4

for I, J being Program of holds I c= stop (I ';' J)