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