let p be Element of HP-WFF ; :: thesis: len p >= 1
per cases ( p is conjunctive or p is conditional or p is simple or p = VERUM ) by Th9;
suppose p is conjunctive ; :: thesis: len p >= 1
then consider r, s being Element of HP-WFF such that
A1: p = r '&' s ;
len p = len (<*2*> ^ (r ^ s)) by A1, FINSEQ_1:32
.= (len <*2*>) + (len (r ^ s)) by FINSEQ_1:22
.= 1 + (len (r ^ s)) by FINSEQ_1:39 ;
hence len p >= 1 by NAT_1:11; :: thesis: verum
end;
suppose p is conditional ; :: thesis: len p >= 1
then consider r, s being Element of HP-WFF such that
A2: p = r => s ;
len p = len (<*1*> ^ (r ^ s)) by A2, FINSEQ_1:32
.= (len <*1*>) + (len (r ^ s)) by FINSEQ_1:22
.= 1 + (len (r ^ s)) by FINSEQ_1:39 ;
hence len p >= 1 by NAT_1:11; :: thesis: verum
end;
suppose p is simple ; :: thesis: len p >= 1
then ex n being Element of NAT st p = prop n ;
hence len p >= 1 by FINSEQ_1:39; :: thesis: verum
end;
suppose p = VERUM ; :: thesis: len p >= 1
hence len p >= 1 by FINSEQ_1:39; :: thesis: verum
end;
end;