let Al be QC-alphabet ; :: thesis: VERUM Al in TAUT Al
TAUT Al is being_a_theory by Th11;
hence VERUM Al in TAUT Al ; :: thesis: verum