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 => q)*>

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 => q)*>

let f be FinSequence of CQC-WFF Al; :: thesis: ( |- (f ^ <*p*>) ^ <*q*> implies |- f ^ <*(p => q)*> )
assume A1: |- (f ^ <*p*>) ^ <*q*> ; :: thesis: |- f ^ <*(p => q)*>
set g1 = ((f ^ <*(p '&' ())*>) ^ <*p*>) ^ <*q*>;
set g = (f ^ <*p*>) ^ <*q*>;
A2: Ant (((f ^ <*(p '&' ())*>) ^ <*p*>) ^ <*q*>) = (f ^ <*(p '&' ())*>) ^ <*p*> by CALCUL_1:5;
Suc ((f ^ <*p*>) ^ <*q*>) = q by CALCUL_1:5;
then A3: Suc (((f ^ <*(p '&' ())*>) ^ <*p*>) ^ <*q*>) = Suc ((f ^ <*p*>) ^ <*q*>) by CALCUL_1:5;
A4: Ant ((f ^ <*p*>) ^ <*q*>) = f ^ <*p*> by CALCUL_1:5;
then A5: 0 + 1 <= len (Ant ((f ^ <*p*>) ^ <*q*>)) by CALCUL_1:10;
A6: |- (f ^ <*(p '&' ())*>) ^ <*(p '&' ())*> by Th21;
then A7: |- (f ^ <*(p '&' ())*>) ^ <*p*> by Th22;
( Ant (Ant ((f ^ <*p*>) ^ <*q*>)) = f & Suc (Ant ((f ^ <*p*>) ^ <*q*>)) = p ) by ;
then |- ((f ^ <*(p '&' ())*>) ^ <*p*>) ^ <*q*> by ;
then A8: |- (f ^ <*(p '&' ())*>) ^ <*q*> by ;
A9: |- (f ^ <*('not' (p '&' ()))*>) ^ <*('not' (p '&' ()))*> by Th21;
|- (f ^ <*(p '&' ())*>) ^ <*()*> by ;
then |- (f ^ <*(p '&' ())*>) ^ <*('not' (p '&' ()))*> by ;
then |- f ^ <*('not' (p '&' ()))*> by ;
hence |- f ^ <*(p => q)*> by QC_LANG2:def 2; :: thesis: verum