set a = atom. 0 ;
A1: atom. 0 is atomic by MODELC_2:def 11;
take atom. 0 ; :: thesis: atom. 0 is neg-inner-most
for G being LTL-formula st G is_subformula_of atom. 0 & G is negative holds
the_argument_of G is atomic

proof

let G be LTL-formula; :: thesis: ( G is_subformula_of atom. 0 & G is negative implies the_argument_of G is atomic )
assume B1: G is_subformula_of atom. 0 ; :: thesis: ( not G is negative or the_argument_of G is atomic )
consider n being Nat, L being FinSequence such that
B2: ( 1 <= n & len L = n & L . 1 = G & L . n = atom. 0 & ( for k being Nat st 1 <= k & k < n holds
ex H1, G1 being LTL-formula st
( L . k = H1 & L . (k + 1) = G1 & H1 is_immediate_constituent_of G1 ) ) ) by B1, MODELC_2:def 22;
B3: n = 1

proof

set k = n - 1;
reconsider k = n - 1 as Nat by B2, NAT_1:21;

now

assume not n = 1 ; :: thesis: contradiction
then 1 < 1 + k by B2, XXREAL_0:1;
then C0: 1 <= k by NAT_1:19;
k < k + 1 by XREAL_1:31;
then consider H1, G1 being LTL-formula such that
C1: ( L . k = H1 & L . (k + 1) = G1 & H1 is_immediate_constituent_of G1 ) by C0, B2;
thus contradiction by A1, B2, C1, MODELC_2:19; :: thesis: verum

end;

hence n = 1 ; :: thesis: verum

end;

thus ( not G is negative or the_argument_of G is atomic ) by A1, B2, B3, MODELC_2:78; :: thesis: verum

end;

hence atom. 0 is neg-inner-most by DefNegIM; :: thesis: verum