let H be LTL-formula; :: thesis: ( ( H is atomic & H . 1 <> 0 & H . 1 <> 1 & H . 1 <> 2 & H . 1 <> 3 & H . 1 <> 4 & H . 1 <> 5 ) or ( H is negative & H . 1 = 0 ) or ( H is conjunctive & H . 1 = 1 ) or ( H is disjunctive & H . 1 = 2 ) or ( H is next & H . 1 = 3 ) or ( H is Until & H . 1 = 4 ) or ( H is Release & H . 1 = 5 ) )
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;
case H is atomic ; :: thesis: ( H . 1 <> 0 & H . 1 <> 1 & H . 1 <> 2 & H . 1 <> 3 & H . 1 <> 4 & H . 1 <> 5 )
hence ( H . 1 <> 0 & H . 1 <> 1 & H . 1 <> 2 & H . 1 <> 3 & H . 1 <> 4 & H . 1 <> 5 ) by Lm9; :: thesis: verum
end;
case H is negative ; :: thesis: H . 1 = 0
hence H . 1 = 0 by Lm3; :: thesis: verum
end;
case H is conjunctive ; :: thesis: H . 1 = 1
hence H . 1 = 1 by Lm4; :: thesis: verum
end;
case H is disjunctive ; :: thesis: H . 1 = 2
hence H . 1 = 2 by Lm5; :: thesis: verum
end;
case H is next ; :: thesis: H . 1 = 3
hence H . 1 = 3 by Lm6; :: thesis: verum
end;
case H is Until ; :: thesis: H . 1 = 4
hence H . 1 = 4 by Lm7; :: thesis: verum
end;
case H is Release ; :: thesis: H . 1 = 5
hence H . 1 = 5 by Lm8; :: thesis: verum
end;
end;