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*> & |- (f ^ <*('not' p)*>) ^ <*q*> holds
|- f ^ <*q*>
let p, q be Element of CQC-WFF Al; :: thesis: for f being FinSequence of CQC-WFF Al st |- (f ^ <*p*>) ^ <*q*> & |- (f ^ <*('not' p)*>) ^ <*q*> holds
|- f ^ <*q*>
let f be FinSequence of CQC-WFF Al; :: 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 ^ <*('not' p)*>) ^ <*q*>) = f ^ <*('not' p)*> by CALCUL_1:5;
A3: Ant ((f ^ <*p*>) ^ <*q*>) = f ^ <*p*> by CALCUL_1:5;
then Suc (Ant ((f ^ <*p*>) ^ <*q*>)) = p by CALCUL_1:5;
then A4: 'not' (Suc (Ant ((f ^ <*p*>) ^ <*q*>))) = Suc (Ant ((f ^ <*('not' p)*>) ^ <*q*>)) by A2, CALCUL_1:5;
A5: ( 1 < len ((f ^ <*p*>) ^ <*q*>) & 1 < len ((f ^ <*('not' p)*>) ^ <*q*>) ) by CALCUL_1:9;
A6: Suc ((f ^ <*p*>) ^ <*q*>) = q by CALCUL_1:5;
then A7: Suc ((f ^ <*p*>) ^ <*q*>) = Suc ((f ^ <*('not' p)*>) ^ <*q*>) by CALCUL_1:5;
A8: Ant (Ant ((f ^ <*p*>) ^ <*q*>)) = f by A3, CALCUL_1:5;
then Ant (Ant ((f ^ <*p*>) ^ <*q*>)) = Ant (Ant ((f ^ <*('not' p)*>) ^ <*q*>)) by A2, CALCUL_1:5;
hence |- f ^ <*q*> by A1, A8, A4, A6, A5, A7, CALCUL_1:37; :: thesis: verum