let Al be QC-alphabet ; :: thesis: for s being QC-formula of Al holds
( s is valid iff s in TAUT Al )
let s be QC-formula of Al; :: thesis: ( s is valid iff s in TAUT Al )
( s is valid iff {} (CQC-WFF Al) |- s ) by Def9;
hence ( s is valid iff s in TAUT Al ) by Def8; :: thesis: verum