let A be QC-alphabet ; :: thesis: for p being Element of CQC-WFF A holds
( index p = 0 A iff p is closed )
let p be Element of CQC-WFF A; :: thesis: ( index p = 0 A iff p is closed )
thus ( index p = 0 A implies p is closed ) :: thesis: ( p is closed implies index p = 0 A )
proof
assume index p = 0 A ; :: thesis: p is closed
then 0 A in NBI p by QC_LANG1:def 35;
then consider t being QC-symbol of A such that
A1: ( t = 0 A & ( for u being QC-symbol of A st t <= u holds
not x. u in still_not-bound_in p ) ) ;
now :: thesis: not still_not-bound_in p <> {}
set a = the Element of still_not-bound_in p;
assume A2: still_not-bound_in p <> {} ; :: thesis: contradiction
then reconsider a = the Element of still_not-bound_in p as bound_QC-variable of A by TARSKI:def 3;
consider u being QC-symbol of A such that
A3: x. u = a by QC_LANG3:30;
not t <= u by A1, A2, A3;
hence contradiction by A1, QC_LANG1:def 36; :: thesis: verum
end;
hence p is closed by QC_LANG1:def 31; :: thesis: verum
end;
assume p is closed ; :: thesis: index p = 0 A
then for t being QC-symbol of A st 0 A <= t holds
not x. t in still_not-bound_in p by QC_LANG1:def 31;
then A4: 0 A in NBI p ;
0 A = min (NBI p)
proof
assume min (NBI p) <> 0 A ; :: thesis: contradiction
then consider t being QC-symbol of A such that
A5: ( 0 A <> t & t = min (NBI p) ) ;
t <= 0 A by A4, A5, QC_LANG1:def 35;
then t < 0 A by A5, QC_LANG1:def 34;
then not 0 A <= t by QC_LANG1:25;
hence contradiction by QC_LANG1:def 36; :: thesis: verum
end;
hence index p = 0 A ; :: thesis: verum