let p be Element of QC-WFF ; :: thesis: for V being non empty Subset of QC-variables holds Vars ('not' p),V = Vars p,V
let V be non empty Subset of QC-variables ; :: thesis: Vars ('not' p),V = Vars p,V
set 'p = 'not' p;
A1: 'not' p is negative by QC_LANG1:def 18;
then the_argument_of ('not' p) = p by QC_LANG1:def 23;
hence Vars ('not' p),V = Vars p,V by A1, Lm2; :: thesis: verum