:: deftheorem Def18 defines the_argument_of MODELC_2:def 18 :
for H being LTL-formula st ( H is negative or H is next ) holds
for b₂ being LTL-formula holds
( ( H is negative implies ( b₂ = the_argument_of H iff 'not' b₂ = H ) ) & ( not H is negative implies ( b₂ = the_argument_of H iff 'X' b₂ = H ) ) );