let il be Instruction-Location of SCM ; :: thesis: Next = NextLoc il
Next = il. SCM ,((locnum il) + 1) by Th55;
hence Next = NextLoc il by AMISTD_1:def 13; :: thesis: verum