let Al be QC-alphabet ; :: thesis: for X being Subset of (CQC-WFF Al)
for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st f is_a_proof_wrt X holds
1 <= len f
let X be Subset of (CQC-WFF Al); :: thesis: for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st f is_a_proof_wrt X holds
1 <= len f
let f be FinSequence of [:(CQC-WFF Al),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 A1: f <> {} ;
0 + 1 <= len f by A1, NAT_1:13;
hence 1 <= len f ; :: thesis: verum