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