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

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

hence
t < index p
by QC_LANG1:25; :: thesis: verum
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;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