let p, q, r be Element of CQC-WFF ; :: thesis: ( (p '&' q) => r is valid implies q => (p => r) is valid )
A1: (q '&' p) => (p '&' q) in TAUT by CQC_THE1:45;
assume (p '&' q) => r in TAUT ; :: according to CQC_THE1:def 10 :: thesis: q => (p => r) is valid
then (q '&' p) => r in TAUT by A1, LUKASI_1:3;
then (q '&' p) => r is valid by CQC_THE1:def 10;
then q => (p => r) is valid by Th3;
hence q => (p => r) in TAUT by CQC_THE1:def 10; :: according to CQC_THE1:def 10 :: thesis: verum