theorem Th30: :: COMPOS_2:31

for S being with_non_trivial_Instructions COM-Struct
for i, j being No-StopCode Instruction of S holds LastLoc (i ';' j) = 2