let A be QC-alphabet ; :: thesis: for r, s being Element of CQC-WFF A holds r => s is Element of CQC-WFF A
let r, s be Element of CQC-WFF A; :: thesis: r => s is Element of CQC-WFF A
r => s = 'not' (r '&' ('not' s)) by QC_LANG2:def 2;
hence r => s is Element of CQC-WFF A ; :: thesis: verum