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 Def11;
A2: ( 3 + 0 < 3 + (3 + n) & 4 + 0 < 4 + (2 + n) ) by XREAL_1:8;
A3: 5 + 0 < 5 + (1 + n) by XREAL_1:8;
( 1 + 0 < 1 + (5 + n) & 2 + 0 < 2 + (4 + n) ) by XREAL_1:8;
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, A2, A3, FINSEQ_1:40; :: thesis: verum