let Al be QC-alphabet ; :: thesis: for Al2 being Al -expanding QC-alphabet
for r, s being Element of CQC-WFF Al
for x being bound_QC-variable of Al holds
( Al2 -Cast (r 'or' s) = (Al2 -Cast r) 'or' (Al2 -Cast s) & Al2 -Cast (Ex (x,r)) = Ex ((Al2 -Cast x),(Al2 -Cast r)) )
let Al2 be Al -expanding QC-alphabet ; :: thesis: for r, s being Element of CQC-WFF Al
for x being bound_QC-variable of Al holds
( Al2 -Cast (r 'or' s) = (Al2 -Cast r) 'or' (Al2 -Cast s) & Al2 -Cast (Ex (x,r)) = Ex ((Al2 -Cast x),(Al2 -Cast r)) )
let r, s be Element of CQC-WFF Al; :: thesis: for x being bound_QC-variable of Al holds
( Al2 -Cast (r 'or' s) = (Al2 -Cast r) 'or' (Al2 -Cast s) & Al2 -Cast (Ex (x,r)) = Ex ((Al2 -Cast x),(Al2 -Cast r)) )
let x be bound_QC-variable of Al; :: thesis: ( Al2 -Cast (r 'or' s) = (Al2 -Cast r) 'or' (Al2 -Cast s) & Al2 -Cast (Ex (x,r)) = Ex ((Al2 -Cast x),(Al2 -Cast r)) )
A1: ( Al2 -Cast ('not' r) = 'not' (Al2 -Cast r) & Al2 -Cast ('not' s) = 'not' (Al2 -Cast s) ) by QC_TRANS:8;
thus Al2 -Cast (r 'or' s) = Al2 -Cast ('not' (('not' r) '&' ('not' s))) by QC_LANG2:def 3
.= 'not' (Al2 -Cast (('not' r) '&' ('not' s))) by QC_TRANS:8
.= 'not' (('not' (Al2 -Cast r)) '&' ('not' (Al2 -Cast s))) by A1, QC_TRANS:8
.= (Al2 -Cast r) 'or' (Al2 -Cast s) by QC_LANG2:def 3 ; :: thesis: Al2 -Cast (Ex (x,r)) = Ex ((Al2 -Cast x),(Al2 -Cast r))
thus Al2 -Cast (Ex (x,r)) = Al2 -Cast ('not' (All (x,('not' r)))) by QC_LANG2:def 5
.= 'not' (Al2 -Cast (All (x,('not' r)))) by QC_TRANS:8
.= 'not' (All ((Al2 -Cast x),(Al2 -Cast ('not' r)))) by QC_TRANS:8
.= 'not' (All ((Al2 -Cast x),('not' (Al2 -Cast r)))) by QC_TRANS:8
.= Ex ((Al2 -Cast x),(Al2 -Cast r)) by QC_LANG2:def 5 ; :: thesis: verum