let A be QC-alphabet ; :: thesis: Fixed (FALSUM A) = {}
thus Fixed (FALSUM A) = Fixed ('not' (VERUM A)) by QC_LANG2:def 1
.= Fixed (VERUM A) by Th39
.= {} by Lm2 ; :: thesis: verum