let H be CTL-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 ) )
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 )
then consider n being Element of NAT such that
A1: H = atom. n ;
A2: 2 + 0 < 2 + (3 + n) by XREAL_1:8;
A3: 4 + 0 < 4 + (1 + n) by XREAL_1:8;
A4: 3 + 0 < 3 + (2 + n) by XREAL_1:8;
1 + 0 < 1 + (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 ) by A1, A2, A4, A3, FINSEQ_1:40; :: thesis: verum