theorem Th20: :: SCMPDS_4:22

for i being Instruction of SCMPDS
for m, n being Nat st i valid_at m & m <= n holds
i valid_at n