let A be QC-alphabet ; :: thesis: for V being non empty Subset of (QC-variables A) holds Vars ((FALSUM A),V) = {}
let V be non empty Subset of (QC-variables A); :: thesis: Vars ((FALSUM A),V) = {}
FALSUM A = 'not' (VERUM A) by QC_LANG2:def 1;
hence Vars ((FALSUM A),V) = Vars ((VERUM A),V) by Th39
.= {} by Lm2 ;
:: thesis: verum