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*> holds
|- f ^ <*(p 'or' q)*>
let p, q be Element of CQC-WFF Al; :: thesis: for f being FinSequence of CQC-WFF Al st |- f ^ <*p*> holds
|- f ^ <*(p 'or' q)*>
let f be FinSequence of CQC-WFF Al; :: thesis: ( |- f ^ <*p*> implies |- f ^ <*(p 'or' q)*> )
set f1 = (f ^ <*(('not' p) '&' ('not' q))*>) ^ <*(('not' p) '&' ('not' q))*>;
assume A1: |- f ^ <*p*> ; :: thesis: |- f ^ <*(p 'or' q)*>
A2: Ant ((f ^ <*(('not' p) '&' ('not' q))*>) ^ <*(('not' p) '&' ('not' q))*>) = f ^ <*(('not' p) '&' ('not' q))*> by Th5;
(len f) + 1 = (len f) + (len <*(('not' p) '&' ('not' q))*>) by FINSEQ_1:39;
then (len f) + 1 = len (Ant ((f ^ <*(('not' p) '&' ('not' q))*>) ^ <*(('not' p) '&' ('not' q))*>)) by A2, FINSEQ_1:22;
then A3: (len f) + 1 in dom (Ant ((f ^ <*(('not' p) '&' ('not' q))*>) ^ <*(('not' p) '&' ('not' q))*>)) by A2, Th10;
A4: Suc ((f ^ <*(('not' p) '&' ('not' q))*>) ^ <*(('not' p) '&' ('not' q))*>) = ('not' p) '&' ('not' q) by Th5;
(Ant ((f ^ <*(('not' p) '&' ('not' q))*>) ^ <*(('not' p) '&' ('not' q))*>)) . ((len f) + 1) = ('not' p) '&' ('not' q) by A2, FINSEQ_1:42;
then Suc ((f ^ <*(('not' p) '&' ('not' q))*>) ^ <*(('not' p) '&' ('not' q))*>) is_tail_of Ant ((f ^ <*(('not' p) '&' ('not' q))*>) ^ <*(('not' p) '&' ('not' q))*>) by A4, A3, Lm2;
then |- (f ^ <*(('not' p) '&' ('not' q))*>) ^ <*('not' p)*> by A2, A4, Th33, Th40;
then |- (f ^ <*p*>) ^ <*('not' (('not' p) '&' ('not' q)))*> by Th49;
then A5: |- (f ^ <*p*>) ^ <*(p 'or' q)*> by QC_LANG2:def 3;
1 <= len (f ^ <*p*>) by Th10;
then |- (Ant (f ^ <*p*>)) ^ <*(p 'or' q)*> by A1, A5, Th45;
hence |- f ^ <*(p 'or' q)*> by Th5; :: thesis: verum