:: deftheorem defines Sub_atomic MODELC_3:def 38 :
for H being LTL-formula holds
( H is Sub_atomic iff ( H is atomic or ex G being LTL-formula st
( G is atomic & H = 'not' G ) ) );