let H be LTL-formula; :: thesis: ( H is Sub_atomic iff ( H is atomic or ( H is negative & the_argument_of H is atomic ) ) )
thus ( not H is Sub_atomic or H is atomic or ( H is negative & the_argument_of H is atomic ) ) :: thesis: ( ( H is atomic or ( H is negative & the_argument_of H is atomic ) ) implies H is Sub_atomic )

proof

assume A1: H is Sub_atomic ; :: thesis: ( H is atomic or ( H is negative & the_argument_of H is atomic ) )

per cases ( H is atomic or ex G being LTL-formula st
( G is atomic & H = 'not' G ) ) by A1, DefSubatomic;

suppose H is atomic ; :: thesis: ( H is atomic or ( H is negative & the_argument_of H is atomic ) )

hence ( H is atomic or ( H is negative & the_argument_of H is atomic ) ) ; :: thesis: verum

end;

suppose ex G being LTL-formula st
( G is atomic & H = 'not' G ) ; :: thesis: ( H is atomic or ( H is negative & the_argument_of H is atomic ) )

then consider G being LTL-formula such that
B1: ( G is atomic & H = 'not' G ) ;
H is negative by B1, MODELC_2:def 12;
hence ( H is atomic or ( H is negative & the_argument_of H is atomic ) ) by B1, MODELC_2:def 18; :: thesis: verum

end;

end;

end;

thus ( ( H is atomic or ( H is negative & the_argument_of H is atomic ) ) implies H is Sub_atomic ) :: thesis: verum

proof

assume A1: ( H is atomic or ( H is negative & the_argument_of H is atomic ) ) ; :: thesis: H is Sub_atomic

per cases ( H is atomic or ( H is negative & the_argument_of H is atomic ) ) by A1;

suppose H is atomic ; :: thesis: H is Sub_atomic

hence H is Sub_atomic by DefSubatomic; :: thesis: verum

end;

suppose B1: ( H is negative & the_argument_of H is atomic ) ; :: thesis: H is Sub_atomic

then H = 'not' (the_argument_of H) by MODELC_2:def 18;
hence H is Sub_atomic by B1, DefSubatomic; :: thesis: verum

end;

end;

end;