let Al be QC-alphabet ; :: thesis: VERUM Al is valid
VERUM Al in TAUT Al by Th41;
hence VERUM Al is valid by Lm13; :: thesis: verum