let p be Element of CQC-WFF ; :: thesis: for i being Element of NAT st x. i in still_not-bound_in p holds
i < index p
let i be Element of NAT ; :: thesis: ( x. i in still_not-bound_in p implies i < index p )
assume A1: x. i in still_not-bound_in p ; :: thesis: i < index p

now

min (NBI p) in NBI p by XXREAL_2:def 7;
then A2: ex k being Element of NAT st
( k = min (NBI p) & ( for i being Element of NAT st k <= i holds
not x. i in still_not-bound_in p ) ) ;
assume min (NBI p) <= i ; :: thesis: contradiction
hence contradiction by A1, A2; :: thesis: verum

end;

hence i < index p ; :: thesis: verum