for H being LTL-formula holds P₁[H]

A1: for H being LTL-formula st H is atomic holds
P₁[H] and
A2: for H being LTL-formula st ( H is negative or H is next ) & P₁[ the_argument_of H] holds
P₁[H] and
A3: for H being LTL-formula st ( H is conjunctive or H is disjunctive or H is Until or H is Release ) & P₁[ the_left_argument_of H] & P₁[ the_right_argument_of H] holds
P₁[H]