let H be LTL-formula; :: thesis: ( H is Release implies ( not H is atomic & not H is negative & not H is conjunctive & not H is disjunctive & not H is next & not H is Until ) )
assume H is Release ; :: thesis: ( not H is atomic & not H is negative & not H is conjunctive & not H is disjunctive & not H is next & not H is Until )
then H . 1 = 5 by Lm8;
hence ( not H is atomic & not H is negative & not H is conjunctive & not H is disjunctive & not H is next & not H is Until ) by Lm3, Lm4, Lm5, Lm6, Lm7, Lm9; :: thesis: verum