theorem Th64: :: MODELC_3:64

for H being LTL-formula holds
( H is Sub_atomic iff ( H is atomic or ( H is negative & the_argument_of H is atomic ) ) )