let Al be QC-alphabet ; :: thesis: for X being Subset of (CQC-WFF Al)
for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st f is_a_proof_wrt X holds
Effect f in Cn X
let X be Subset of (CQC-WFF Al); :: thesis: for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st f is_a_proof_wrt X holds
Effect f in Cn X
let f be FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:]; :: thesis: ( f is_a_proof_wrt X implies Effect f in Cn X )
assume A1: f is_a_proof_wrt X ; :: thesis: Effect f in Cn X
then A2: 1 <= len f by Th21;
then A3: (f . (len f)) `1 in Cn X by A1, Th27;
f <> {} by A2;
hence Effect f in Cn X by A3, Def6; :: thesis: verum