let p, q be Element of CQC-WFF ; :: thesis: for f being FinSequence of CQC-WFF st |- (f ^ <*p*>) ^ <*q*> holds
|- f ^ <*(p => q)*>
let f be FinSequence of CQC-WFF ; :: thesis: ( |- (f ^ <*p*>) ^ <*q*> implies |- f ^ <*(p => q)*> )
assume A1: |- (f ^ <*p*>) ^ <*q*> ; :: thesis: |- f ^ <*(p => q)*>
A2: |- (f ^ <*(p '&' ('not' q))*>) ^ <*(p '&' ('not' q))*> by Th21;
then A3: |- (f ^ <*(p '&' ('not' q))*>) ^ <*p*> by Th22;
set g = (f ^ <*p*>) ^ <*q*>;
A4: ( Ant ((f ^ <*p*>) ^ <*q*>) = f ^ <*p*> & Suc ((f ^ <*p*>) ^ <*q*>) = q ) by CALCUL_1:5;
then A5: ( Ant (Ant ((f ^ <*p*>) ^ <*q*>)) = f & Suc (Ant ((f ^ <*p*>) ^ <*q*>)) = p ) by CALCUL_1:5;
A6: 0 + 1 <= len (Ant ((f ^ <*p*>) ^ <*q*>)) by A4, CALCUL_1:10;
set g1 = ((f ^ <*(p '&' ('not' q))*>) ^ <*p*>) ^ <*q*>;
( Suc (((f ^ <*(p '&' ('not' q))*>) ^ <*p*>) ^ <*q*>) = Suc ((f ^ <*p*>) ^ <*q*>) & Ant (((f ^ <*(p '&' ('not' q))*>) ^ <*p*>) ^ <*q*>) = (f ^ <*(p '&' ('not' q))*>) ^ <*p*> ) by A4, CALCUL_1:5;
then |- ((f ^ <*(p '&' ('not' q))*>) ^ <*p*>) ^ <*q*> by A1, A5, A6, CALCUL_1:13, CALCUL_1:36;
then A7: |- (f ^ <*(p '&' ('not' q))*>) ^ <*q*> by A3, Th24;
|- (f ^ <*(p '&' ('not' q))*>) ^ <*('not' q)*> by A2, Th23;
then A8: |- (f ^ <*(p '&' ('not' q))*>) ^ <*('not' (p '&' ('not' q)))*> by A7, Th25;
|- (f ^ <*('not' (p '&' ('not' q)))*>) ^ <*('not' (p '&' ('not' q)))*> by Th21;
then |- f ^ <*('not' (p '&' ('not' q)))*> by A8, Th26;
hence |- f ^ <*(p => q)*> by QC_LANG2:def 2; :: thesis: verum