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