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 ;
A3: 5 + 0 < 5 + (1 + n) by XREAL_1:8;
thus ( 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; :: thesis: verum