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