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 A1: f is_a_proof_wrt X ; :: thesis: rng f <> {}
A2: f <> {} by A1, Def5;
thus rng f <> {} by A2, RELAT_1:64; :: thesis: verum