let a be Int_position; :: thesis: 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)) )

let i be Integer; :: thesis: 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)) )

let n, m be Nat; :: thesis: for I being Program of holds

( m < (card I) + 3 iff m in dom (for-up (a,i,n,I)) )

let I be Program of ; :: thesis: ( m < (card I) + 3 iff m in dom (for-up (a,i,n,I)) )

card (for-up (a,i,n,I)) = (card I) + 3 by Th30;

hence ( m < (card I) + 3 iff m in dom (for-up (a,i,n,I)) ) by AFINSQ_1:66; :: thesis: verum

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

let i be Integer; :: thesis: 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)) )

let n, m be Nat; :: thesis: for I being Program of holds

( m < (card I) + 3 iff m in dom (for-up (a,i,n,I)) )

let I be Program of ; :: thesis: ( m < (card I) + 3 iff m in dom (for-up (a,i,n,I)) )

card (for-up (a,i,n,I)) = (card I) + 3 by Th30;

hence ( m < (card I) + 3 iff m in dom (for-up (a,i,n,I)) ) by AFINSQ_1:66; :: thesis: verum