let Al be QC-alphabet ; 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; for f being FinSequence of CQC-WFF Al st |- f ^ <*p*> holds
|- f ^ <*(p 'or' q)*>
let f be FinSequence of CQC-WFF Al; ( |- f ^ <*p*> implies |- f ^ <*(p 'or' q)*> )
set f1 = (f ^ <*(('not' p) '&' ('not' q))*>) ^ <*(('not' p) '&' ('not' q))*>;
assume A1:
|- f ^ <*p*>
; |- 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; verum