theorem Th1: :: SCMPDS_5:12

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