thus H₁( VERUM ) = {} bound_QC-variables from QC_LANG3:sch 3(Lm1)
.= {} ; :: thesis: verum