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