theorem Th31: :: SCMPDS_7:33

for a being Int_position
for i being Integer
for n, m being Nat
for I being Program of holds
( m < (card I) + 3 iff m in dom (for-up (a,i,n,I)) )