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

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