let X be Subset of CQC-WFF; :: thesis: for f being FinSequence of [:CQC-WFF,Proof_Step_Kinds:] st f is_a_proof_wrt X holds
rng f <> {}
let f be FinSequence of [:CQC-WFF,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