theorem Th15: :: SCMPDS_8:17

for a being Int_position
for i being Integer
for I being Program of SCMPDS holds card (while>0 (a,i,I)) = (card I) + 2