let s be QC-formula; :: thesis: ( s is valid iff s in TAUT )
( s is valid iff {} CQC-WFF |- s ) by Def10;
hence ( s is valid iff s in TAUT ) by Def9; :: thesis: verum