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