let V be non empty Subset of QC-variables; :: thesis: Vars (FALSUM,V) = {}
thus Vars (FALSUM,V) = Vars (VERUM,V) by Th50, QC_LANG2:def 1
.= {} by Lm2 ; :: thesis: verum