set a = atom. 0;
take atom. 0 ; :: thesis: atom. 0 is neg-inner-most
A1: atom. 0 is atomic ;
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 G is_subformula_of atom. 0 ; :: thesis: ( not G is negative or the_argument_of G is atomic )
then consider n being Nat, L being FinSequence such that
A2: 1 <= n and
len L = n and
A3: L . 1 = G and
A4: L . n = atom. 0 and
A5: 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 ) ;
n = 1

proof

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

now :: thesis: n = 1

assume not n = 1 ; :: thesis: contradiction
then 1 < 1 + k by A2, XXREAL_0:1;
then A6: 1 <= k by NAT_1:19;
k < k + 1 by XREAL_1:29;
then ex H1, G1 being LTL-formula st
( L . k = H1 & L . (k + 1) = G1 & H1 is_immediate_constituent_of G1 ) by A5, A6;
hence contradiction by A1, A4, MODELC_2:19; :: thesis: verum

end;

hence n = 1 ; :: thesis: verum

end;

hence ( not G is negative or the_argument_of G is atomic ) by A1, A3, A4, MODELC_2:78; :: thesis: verum

end;

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