let A be QC-alphabet ; :: thesis: |- TAUT A
A1: ( |- TAUT A iff {} (CQC-WFF A) |- TAUT A ) by Th15;
{} (CQC-WFF A) |- TAUT A by Th13;
hence |- TAUT A by A1; :: thesis: verum