let A be QC-alphabet ; :: thesis: still_not-bound_in (FALSUM A) = {}
still_not-bound_in (FALSUM A) = still_not-bound_in ('not' (VERUM A)) by QC_LANG2:def 1
.= still_not-bound_in (VERUM A) by Th7
.= {} by Th3 ;
hence still_not-bound_in (FALSUM A) = {} ; :: thesis: verum