let p be Element of CQC-WFF ; :: thesis: ( index p = 0 iff p is closed )
thus ( index p = 0 implies p is closed ) :: thesis: ( p is closed implies index p = 0 )

proof

assume index p = 0 ; :: thesis: p is closed
then 0 in NBI p by XXREAL_2:def 7;
then A1: ex k being Element of NAT st
( k = 0 & ( for i being Element of NAT st k <= i holds
not x. i in still_not-bound_in p ) ) ;

now

consider a being Element of still_not-bound_in p;
assume A2: still_not-bound_in p <> {} ; :: thesis: contradiction
then reconsider a = a as bound_QC-variable by TARSKI:def 3;
ex i being Element of NAT st x. i = a by QC_LANG3:36;
hence contradiction by A1, A2; :: thesis: verum

end;

hence p is closed by QC_LANG1:def 30; :: thesis: verum

end;

assume p is closed ; :: thesis: index p = 0
then for i being Element of NAT st 0 <= i holds
not x. i in still_not-bound_in p by QC_LANG1:def 30;
then 0 in NBI p ;
hence index p = 0 by XXREAL_2:def 7; :: thesis: verum