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