let H be CTL-formula; :: thesis: 1 <= len H
per cases ( H is atomic or H is negative or H is conjunctive or H is ExistNext or H is ExistGlobal or H is ExistUntill ) by Th2;
suppose H is atomic ; :: thesis: 1 <= len H
then ex n being Element of 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 CTL-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 CTL-formula such that
A2: H = F '&' G ;
A3: 1 <= 1 + (len F) by NAT_1:11;
A4: 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, A4, XXREAL_0:2; :: thesis: verum
end;
suppose H is ExistNext ; :: thesis: 1 <= len H
then consider H1 being CTL-formula such that
A5: H = EX H1 ;
len H = 1 + (len H1) by A5, FINSEQ_5:8;
hence 1 <= len H by NAT_1:11; :: thesis: verum
end;
suppose H is ExistGlobal ; :: thesis: 1 <= len H
then consider H1 being CTL-formula such that
A6: H = EG 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 ExistUntill ; :: thesis: 1 <= len H
then consider F, G being CTL-formula such that
A7: H = F EU G ;
A8: 1 <= 1 + (len F) by NAT_1:11;
A9: 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, A9, XXREAL_0:2; :: thesis: verum
end;
end;