let H be LTL-formula; :: thesis: ( not H is neg-inner-most or H is Sub_atomic or H is conjunctive or H is disjunctive or H is next or H is Until or H is Release )
assume A1: H is neg-inner-most ; :: thesis: ( H is Sub_atomic or H is conjunctive or H is disjunctive or H is next or H is Until or H is Release )

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 MODELC_2:2;

suppose H is atomic ; :: thesis: ( H is Sub_atomic or H is conjunctive or H is disjunctive or H is next or H is Until or H is Release )

hence ( H is Sub_atomic or H is conjunctive or H is disjunctive or H is next or H is Until or H is Release ) ; :: thesis: verum

end;

suppose A2: H is negative ; :: thesis: ( H is Sub_atomic or H is conjunctive or H is disjunctive or H is next or H is Until or H is Release )

set G = the_argument_of H;
A3: the_argument_of H is atomic by A1, A2;
H = 'not' (the_argument_of H) by A2, MODELC_2:def 18;
hence ( H is Sub_atomic or H is conjunctive or H is disjunctive or H is next or H is Until or H is Release ) by A3; :: thesis: verum

end;

suppose ( H is conjunctive or H is disjunctive or H is next or H is Until or H is Release ) ; :: thesis: ( H is Sub_atomic or H is conjunctive or H is disjunctive or H is next or H is Until or H is Release )

hence ( H is Sub_atomic or H is conjunctive or H is disjunctive or H is next or H is Until or H is Release ) ; :: thesis: verum

end;

end;