let H be LTL-formula; :: thesis: ( H is atomic implies ( not H . 1 = 0 & not H . 1 = 1 & not H . 1 = 2 & not H . 1 = 3 & not H . 1 = 4 & not H . 1 = 5 ) )
assume H is atomic ; :: thesis: ( not H . 1 = 0 & not H . 1 = 1 & not H . 1 = 2 & not H . 1 = 3 & not H . 1 = 4 & not H . 1 = 5 )
then consider n being Nat such that
A1: H = atom. n by Def14;
A3: 1 + 0 < 1 + (5 + n) by XREAL_1:10;
A4: 2 + 0 < 2 + (4 + n) by XREAL_1:10;
A5: 3 + 0 < 3 + (3 + n) by XREAL_1:10;
A6: 4 + 0 < 4 + (2 + n) by XREAL_1:10;
5 + 0 < 5 + (1 + n) by XREAL_1:10;
hence ( not H . 1 = 0 & not H . 1 = 1 & not H . 1 = 2 & not H . 1 = 3 & not H . 1 = 4 & not H . 1 = 5 ) by A1, A3, A4, A5, A6, FINSEQ_1:57; :: thesis: verum