let A be QC-alphabet ; :: thesis: for s, h being QC-formula of A
for x being bound_QC-variable of A holds (s 'or' h) . x = (s . x) 'or' (h . x)
let s, h be QC-formula of A; :: thesis: for x being bound_QC-variable of A holds (s 'or' h) . x = (s . x) 'or' (h . x)
let x be bound_QC-variable of A; :: thesis: (s 'or' h) . x = (s . x) 'or' (h . x)
thus (s 'or' h) . x = ('not' (('not' s) '&' ('not' h))) . x by QC_LANG2:def 3
.= 'not' ((('not' s) '&' ('not' h)) . x) by CQC_LANG:19
.= 'not' ((('not' s) . x) '&' (('not' h) . x)) by CQC_LANG:21
.= 'not' (('not' (s . x)) '&' (('not' h) . x)) by CQC_LANG:19
.= 'not' (('not' (s . x)) '&' ('not' (h . x))) by CQC_LANG:19
.= (s . x) 'or' (h . x) by QC_LANG2:def 3 ; :: thesis: verum