let p, q be Element of CQC-WFF ; :: thesis: for f being FinSequence of CQC-WFF st |- (f ^ <*p*>) ^ <*q*> & |- (f ^ <*('not' p)*>) ^ <*q*> holds
|- f ^ <*q*>
let f be FinSequence of CQC-WFF ; :: thesis: ( |- (f ^ <*p*>) ^ <*q*> & |- (f ^ <*('not' p)*>) ^ <*q*> implies |- f ^ <*q*> )
set f1 = (f ^ <*p*>) ^ <*q*>;
set f2 = (f ^ <*('not' p)*>) ^ <*q*>;
assume A1: ( |- (f ^ <*p*>) ^ <*q*> & |- (f ^ <*('not' p)*>) ^ <*q*> ) ; :: thesis: |- f ^ <*q*>
A2: ( Ant ((f ^ <*p*>) ^ <*q*>) = f ^ <*p*> & Ant ((f ^ <*('not' p)*>) ^ <*q*>) = f ^ <*('not' p)*> ) by CALCUL_1:5;
then A3: ( Ant (Ant ((f ^ <*p*>) ^ <*q*>)) = f & Suc (Ant ((f ^ <*p*>) ^ <*q*>)) = p ) by CALCUL_1:5;
then A4: ( Ant (Ant ((f ^ <*p*>) ^ <*q*>)) = Ant (Ant ((f ^ <*('not' p)*>) ^ <*q*>)) & 'not' (Suc (Ant ((f ^ <*p*>) ^ <*q*>))) = Suc (Ant ((f ^ <*('not' p)*>) ^ <*q*>)) ) by A2, CALCUL_1:5;
A5: ( Suc ((f ^ <*p*>) ^ <*q*>) = q & 1 < len ((f ^ <*p*>) ^ <*q*>) & 1 < len ((f ^ <*('not' p)*>) ^ <*q*>) ) by CALCUL_1:5, CALCUL_1:9;
then Suc ((f ^ <*p*>) ^ <*q*>) = Suc ((f ^ <*('not' p)*>) ^ <*q*>) by CALCUL_1:5;
hence |- f ^ <*q*> by A1, A3, A4, A5, CALCUL_1:37; :: thesis: verum