let A be QC-alphabet ; :: thesis: for F being Element of QC-WFF A holds 1 <= len (@ F)
let F be Element of QC-WFF A; :: thesis: 1 <= len (@ F)

now :: thesis: 1 <= len (@ F)

per cases ( F = VERUM A or F is atomic or F is negative or F is conjunctive or F is universal ) by Th9;

suppose F = VERUM A ; :: thesis: 1 <= len (@ F)

hence 1 <= len (@ F) by FINSEQ_1:39; :: thesis: verum

end;

suppose F is atomic ; :: thesis: 1 <= len (@ F)

then consider k being Nat, p being QC-pred_symbol of k,A, ll being QC-variable_list of k,A such that
A1: F = p ! ll ;
@ F = <*p*> ^ ll by A1, Th8;
then len (@ F) = (len <*p*>) + (len ll) by FINSEQ_1:22
.= 1 + (len ll) by FINSEQ_1:39 ;
hence 1 <= len (@ F) by NAT_1:11; :: thesis: verum

end;

suppose F is negative ; :: thesis: 1 <= len (@ F)

then consider p being Element of QC-WFF A such that
A2: F = 'not' p ;
len (@ F) = (len <*[1,0]*>) + (len (@ p)) by A2, FINSEQ_1:22
.= 1 + (len (@ p)) by FINSEQ_1:39 ;
hence 1 <= len (@ F) by NAT_1:11; :: thesis: verum

end;

suppose F is conjunctive ; :: thesis: 1 <= len (@ F)

then consider p, q being Element of QC-WFF A such that
A3: F = p '&' q ;
@ F = <*[2,0]*> ^ ((@ p) ^ (@ q)) by A3, FINSEQ_1:32;
then len (@ F) = (len <*[2,0]*>) + (len ((@ p) ^ (@ q))) by FINSEQ_1:22
.= 1 + (len ((@ p) ^ (@ q))) by FINSEQ_1:39 ;
hence 1 <= len (@ F) by NAT_1:11; :: thesis: verum

end;

suppose F is universal ; :: thesis: 1 <= len (@ F)

then consider x being bound_QC-variable of A, p being Element of QC-WFF A such that
A4: F = All (x,p) ;
@ F = <*[3,0]*> ^ (<*x*> ^ (@ p)) by A4, FINSEQ_1:32;
then len (@ F) = (len <*[3,0]*>) + (len (<*x*> ^ (@ p))) by FINSEQ_1:22
.= 1 + (len (<*x*> ^ (@ p))) by FINSEQ_1:39 ;
hence 1 <= len (@ F) by NAT_1:11; :: thesis: verum

end;

end;

end;

hence 1 <= len (@ F) ; :: thesis: verum