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 A1: f is_a_proof_wrt X ; :: thesis: 1 <= len f
A2: f <> {} by A1, Def5;
A3: 0 <= len f by NAT_1:2;
A4: 0 + 1 <= len f by A2, A3, NAT_1:13;
thus 1 <= len f by A4; :: thesis: verum