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

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