let X be Subset of MC-wff; :: thesis: for f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st f is_a_proof_wrt_IPC X holds
1 <= len f
let f be FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:]; :: thesis: ( f is_a_proof_wrt_IPC X implies 1 <= len f )
assume f is_a_proof_wrt_IPC X ; :: thesis: 1 <= len f
then 0 + 1 <= len f by NAT_1:13;
hence 1 <= len f ; :: thesis: verum