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
1 <= len f
let f be FinSequence of [:CQC-WFF,Proof_Step_Kinds:]; :: thesis: ( f is_a_proof_wrt X implies 1 <= len f )
assume f is_a_proof_wrt X ; :: thesis: 1 <= len f
then A2: f <> {} by Def5;
0 <= len f by NAT_1:2;
then 0 + 1 <= len f by A2, NAT_1:13;
hence 1 <= len f ; :: thesis: verum