let A be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF A st p => q is valid holds
p |- q
let p, q be Element of CQC-WFF A; :: 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 ; :: thesis: verum