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;

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 A2: 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 H is negative ;
hence ( H is atomic or ( H is negative & the_argument_of H is atomic ) ) by A2, 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 A3: ( 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 A3;

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

hence H is Sub_atomic ; :: thesis: verum

end;

suppose A4: ( 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 A4; :: thesis: verum

end;

end;

end;