let Al be QC-alphabet ; :: thesis: for p, q, r being Element of CQC-WFF Al
for X being Subset of (CQC-WFF Al) holds (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in { F where F is Element of CQC-WFF Al : ex f being FinSequence of st
( f is_a_proof_wrt X & Effect f = F )
}

let p, q, r be Element of CQC-WFF Al; :: thesis: for X being Subset of (CQC-WFF Al) holds (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in { F where F is Element of CQC-WFF Al : ex f being FinSequence of st
( f is_a_proof_wrt X & Effect f = F )
}

let X be Subset of (CQC-WFF Al); :: thesis: (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in { F where F is Element of CQC-WFF Al : ex f being FinSequence of st
( f is_a_proof_wrt X & Effect f = F )
}

reconsider pp = [((p => q) => (('not' (q '&' r)) => ('not' (p '&' r)))),4] as Element of by ;
set f = <*pp*>;
A1: len <*pp*> = 1 by FINSEQ_1:40;
A2: <*pp*> . 1 = pp by FINSEQ_1:40;
then (<*pp*> . (len <*pp*>)) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) by A1;
then A3: Effect <*pp*> = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) by Def6;
for n being Nat st 1 <= n & n <= len <*pp*> holds
<*pp*>,n is_a_correct_step_wrt X
proof
let n be Nat; :: thesis: ( 1 <= n & n <= len <*pp*> implies <*pp*>,n is_a_correct_step_wrt X )
assume ( 1 <= n & n <= len <*pp*> ) ; :: thesis:
then A4: n = 1 by ;
A5: (<*pp*> . 1) `2 = 4 by A2;
(<*pp*> . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) by A2, A4;
hence <*pp*>,n is_a_correct_step_wrt X by A4, A5, Def4; :: thesis: verum
end;
then <*pp*> is_a_proof_wrt X ;
hence (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) in { F where F is Element of CQC-WFF Al : ex f being FinSequence of st
( f is_a_proof_wrt X & Effect f = F )
}
by A3; :: thesis: verum