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