let Al be QC-alphabet ; :: thesis: for p being Element of CQC-WFF Al st still_not-bound_in p c= Bound_Vars p holds
still_not-bound_in ('not' p) c= Bound_Vars ('not' p)
let p be Element of CQC-WFF Al; :: thesis: ( still_not-bound_in p c= Bound_Vars p implies still_not-bound_in ('not' p) c= Bound_Vars ('not' p) )
'not' p is negative by QC_LANG1:def 19;
then Bound_Vars ('not' p) = Bound_Vars (the_argument_of ('not' p)) by SUBSTUT1:4;
then A1: Bound_Vars ('not' p) = Bound_Vars p by QC_LANG2:1;
assume still_not-bound_in p c= Bound_Vars p ; :: thesis: still_not-bound_in ('not' p) c= Bound_Vars ('not' p)
hence still_not-bound_in ('not' p) c= Bound_Vars ('not' p) by A1, QC_LANG3:7; :: thesis: verum