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*> & |- (f ^ <*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*> & |- (f ^ <*p*>) ^ <*q*> holds
|- f ^ <*q*>
let f be FinSequence of CQC-WFF Al; :: thesis: ( |- f ^ <*p*> & |- (f ^ <*p*>) ^ <*q*> implies |- f ^ <*q*> )
A1: 1 <= len (f ^ <*p*>) by CALCUL_1:10;
assume ( |- f ^ <*p*> & |- (f ^ <*p*>) ^ <*q*> ) ; :: thesis: |- f ^ <*q*>
then |- (Ant (f ^ <*p*>)) ^ <*q*> by A1, CALCUL_1:45;
hence |- f ^ <*q*> by CALCUL_1:5; :: thesis: verum