theorem Th5: :: SCMPDS_8:7

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)) )