let F be Element of QC-WFF ; :: thesis: 1 <= len (@ F)

now

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

suppose F = VERUM ; :: 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 Element of NAT , p being QC-pred_symbol of k, ll being QC-variable_list of k such that
A1: F = p ! ll by Def17;
@ F = <*p*> ^ ll by A1, Th23;
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 such that
A2: F = 'not' p by Def18;
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 such that
A3: F = p '&' q by Def19;
@ 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, p being Element of QC-WFF such that
A4: F = All (x,p) by Def20;
@ 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