let S be with_non_trivial_Instructions COM-Struct ; :: thesis: for i, j being No-StopCode Instruction of S holds LastLoc (i ';' j) = 2
let i, j be No-StopCode Instruction of S; :: thesis: LastLoc (i ';' j) = 2
thus LastLoc (i ';' j) = (card (i ';' j)) - 1 by AFINSQ_1:91
.= 3 - 1 by Th12
.= 2 ; :: thesis: verum