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
rng f <> {}
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
rng f <> {}
let f be FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:]; :: thesis: ( f is_a_proof_wrt X implies rng f <> {} )
assume f is_a_proof_wrt X ; :: thesis: rng f <> {}
then f <> {} by Def5;
hence rng f <> {} by RELAT_1:41; :: thesis: verum