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