let S be with_non_trivial_Instructions COM-Struct ; :: thesis: for i, j being No-StopCode Instruction of S holds card (i ';' j) = 3
let i, j be No-StopCode Instruction of S; :: thesis: card (i ';' j) = 3
thus card (i ';' j) = ((card (Macro i)) + (card (Macro j))) - 1 by COMPOS_1:20
.= (2 + (card (Macro i))) - 1 by COMPOS_1:56
.= (2 + 2) - 1 by COMPOS_1:56
.= 3 ; :: thesis: verum