for H being LTL-formula st H is negative holds
H = 'not' (the_argument_of H) by Def18;