let X be Subset of CQC-WFF ; for f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st f is_a_proof_wrt X holds
Effect f in Cn X
let f be FinSequence of [:CQC-WFF ,Proof_Step_Kinds :]; ( f is_a_proof_wrt X implies Effect f in Cn X )
assume A1:
f is_a_proof_wrt X
; Effect f in Cn X
A2:
1 <= len f
by A1, Th58;
A3:
(f . (len f)) `1 in Cn X
by A1, A2, Th64;
A4:
f <> {}
by A2;
thus
Effect f in Cn X
by A3, A4, Def6; verum