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 f <> {} by Def5;
then ( len f <> 0 & 0 <= len f ) by NAT_1:2;
then 0 + 1 <= len f by NAT_1:13;
hence 1 <= len f ; :: thesis: verum