let A be QC-alphabet ; :: thesis: for t being QC-symbol of A
for p being Element of CQC-WFF A st x. t in still_not-bound_in p holds
t < index p
let t be QC-symbol of A; :: thesis: for p being Element of CQC-WFF A st x. t in still_not-bound_in p holds
t < index p
let p be Element of CQC-WFF A; :: thesis: ( x. t in still_not-bound_in p implies t < index p )
assume A1: x. t in still_not-bound_in p ; :: thesis: t < index p

now :: thesis: not min (NBI p) <= t

min (NBI p) in NBI p by QC_LANG1:def 35;
then A2: ex u being QC-symbol of A st
( u = min (NBI p) & ( for t being QC-symbol of A st u <= t holds
not x. t in still_not-bound_in p ) ) ;
assume min (NBI p) <= t ; :: thesis: contradiction
hence contradiction by A1, A2; :: thesis: verum

end;

hence t < index p by QC_LANG1:25; :: thesis: verum