theorem Th16: :: SCMPDS_8:18

for a being Int_position
for i being Integer
for m being Nat
for I being Program of SCMPDS holds
( m < (card I) + 2 iff m in dom (while>0 (a,i,I)) )