let Al be QC-alphabet ; :: thesis: for p, q being Element of CQC-WFF Al
for f being FinSequence of CQC-WFF Al st |- f ^ <*(p '&' q)*> holds
|- f ^ <*p*>
let p, q be Element of CQC-WFF Al; :: thesis: for f being FinSequence of CQC-WFF Al st |- f ^ <*(p '&' q)*> holds
|- f ^ <*p*>
let f be FinSequence of CQC-WFF Al; :: thesis: ( |- f ^ <*(p '&' q)*> implies |- f ^ <*p*> )
A1: p '&' q = Suc (f ^ <*(p '&' q)*>) by CALCUL_1:5;
assume |- f ^ <*(p '&' q)*> ; :: thesis: |- f ^ <*p*>
then |- (Ant (f ^ <*(p '&' q)*>)) ^ <*p*> by A1, CALCUL_1:40;
hence |- f ^ <*p*> by CALCUL_1:5; :: thesis: verum