let N be with_non-empty_elements set ; :: thesis: for l being Instruction-Location of STC N holds SUCC l = {l,(NextLoc l)}
let l be Instruction-Location of STC N; :: thesis: SUCC l = {l,(NextLoc l)}
set M = STC N;
consider k being natural number such that
A1: l = il. (STC N),k by Th26;
A2: k = locnum l by A1, Def13;
thus SUCC l = {k,(k + 1)} by A1, Th24, Th37
.= {k,(il. (STC N),(k + 1))} by Th37
.= {l,(NextLoc l)} by A1, A2, Th37 ; :: thesis: verum