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 consider n being Nat such that
A1: H = atom. n by Def14;
thus 1 <= len H by A1, FINSEQ_1:57; :: thesis: verum

end;

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

then consider H1 being LTL-formula such that
A2: H = 'not' H1 by Def15;
len H = 1 + (len H1) by A2, 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
A3: H = F '&' G by Def16;
A4: len H = (1 + (len F)) + (len G) by A3, Lm2;
( 1 <= 1 + (len F) & 1 + (len F) <= (1 + (len F)) + (len G) ) by NAT_1:11;
hence 1 <= len H by A4, XXREAL_0:2; :: thesis: verum

end;

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

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

end;

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

then consider H1 being LTL-formula such that
A7: H = 'X' H1 by Def18;
len H = 1 + (len H1) by A7, 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
A8: H = F 'U' G by Def19;
A9: len H = (1 + (len F)) + (len G) by A8, Lm2;
( 1 <= 1 + (len F) & 1 + (len F) <= (1 + (len F)) + (len G) ) by NAT_1:11;
hence 1 <= len H by A9, XXREAL_0:2; :: thesis: verum

end;

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

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

end;

end;