let H be LTL-formula; :: thesis: 1 <= len H

per cases ( H is atomic or H is negative or H is conjunctive or H is disjunctive or H is next or H is Until or H is Release ) by Th2;

suppose H is atomic ; :: thesis: 1 <= len H

then ex n being Nat st H = atom. n ;
hence 1 <= len H by FINSEQ_1:40; :: thesis: verum

end;

suppose H is negative ; :: thesis: 1 <= len H

then consider H1 being LTL-formula such that
A1: H = 'not' H1 ;
len H = 1 + (len H1) by A1, FINSEQ_5:8;
hence 1 <= len H by NAT_1:11; :: thesis: verum

end;

suppose H is conjunctive ; :: thesis: 1 <= len H

then consider F, G being LTL-formula such that
A2: H = F '&' G ;
A3: ( 1 <= 1 + (len F) & 1 + (len F) <= (1 + (len F)) + (len G) ) by NAT_1:11;
len H = (1 + (len F)) + (len G) by A2, Lm2;
hence 1 <= len H by A3, XXREAL_0:2; :: thesis: verum

end;

suppose H is disjunctive ; :: thesis: 1 <= len H

then consider F, G being LTL-formula such that
A4: H = F 'or' G ;
A5: ( 1 <= 1 + (len F) & 1 + (len F) <= (1 + (len F)) + (len G) ) by NAT_1:11;
len H = (1 + (len F)) + (len G) by A4, Lm2;
hence 1 <= len H by A5, XXREAL_0:2; :: thesis: verum

end;

suppose H is next ; :: thesis: 1 <= len H

then consider H1 being LTL-formula such that
A6: H = 'X' H1 ;
len H = 1 + (len H1) by A6, FINSEQ_5:8;
hence 1 <= len H by NAT_1:11; :: thesis: verum

end;

suppose H is Until ; :: thesis: 1 <= len H

then consider F, G being LTL-formula such that
A7: H = F 'U' G ;
A8: ( 1 <= 1 + (len F) & 1 + (len F) <= (1 + (len F)) + (len G) ) by NAT_1:11;
len H = (1 + (len F)) + (len G) by A7, Lm2;
hence 1 <= len H by A8, XXREAL_0:2; :: thesis: verum

end;

suppose H is Release ; :: thesis: 1 <= len H

then consider F, G being LTL-formula such that
A9: H = F 'R' G ;
A10: ( 1 <= 1 + (len F) & 1 + (len F) <= (1 + (len F)) + (len G) ) by NAT_1:11;
len H = (1 + (len F)) + (len G) by A9, Lm2;
hence 1 <= len H by A10, XXREAL_0:2; :: thesis: verum

end;

end;