let A be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF A st p is valid holds
q => p is valid
let p, q be Element of CQC-WFF A; :: thesis: ( p is valid implies q => p is valid )
assume p is valid ; :: thesis: q => p is valid
then p in TAUT A by CQC_THE1:def 10;
hence q => p in TAUT A by Th13; :: according to CQC_THE1:def 10 :: thesis: verum