let A be QC-alphabet ; :: thesis: for p, q being Element of QC-WFF A holds Fixed (p 'or' q) = (Fixed p) \/ (Fixed q)
let p, q be Element of QC-WFF A; :: thesis: Fixed (p 'or' q) = (Fixed p) \/ (Fixed q)
p 'or' q = 'not' (('not' p) '&' ('not' q)) by QC_LANG2:def 3;
hence Fixed (p 'or' q) = Fixed (('not' p) '&' ('not' q)) by Th39
.= (Fixed ('not' p)) \/ (Fixed ('not' q)) by Th42
.= (Fixed p) \/ (Fixed ('not' q)) by Th39
.= (Fixed p) \/ (Fixed q) by Th39 ;
:: thesis: verum