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:98;
then {p} |- q by CQC_THE1:92, CQC_THE2:91;
hence p |- q by Def1; :: thesis: verum