let p, q be Element of CQC-WFF ; :: thesis: ( p => q is valid implies p |- q )
assume p => q is valid ; :: thesis: p |- q
then {p} |- p => q by CQC_THE1:59;
then {p} |- q by CQC_THE1:55, CQC_THE2:87;
hence p |- q by Def1; :: thesis: verum