A2: ( H is Until implies ex G, H1 being LTL-formula st H1 'U' G = H )

proof

assume H is Until ; :: thesis: ex G, H1 being LTL-formula st H1 'U' G = H
then consider G, F being LTL-formula such that
A3: G 'U' F = H by Def16;
take F ; :: thesis: ex H1 being LTL-formula st H1 'U' F = H
thus ex H1 being LTL-formula st H1 'U' F = H by A3; :: thesis: verum

end;

A4: ( H is disjunctive implies ex G, H1 being LTL-formula st H1 'or' G = H )

proof

assume H is disjunctive ; :: thesis: ex G, H1 being LTL-formula st H1 'or' G = H
then consider G, F being LTL-formula such that
A5: G 'or' F = H by Def14;
take F ; :: thesis: ex H1 being LTL-formula st H1 'or' F = H
thus ex H1 being LTL-formula st H1 'or' F = H by A5; :: thesis: verum

end;

A6: ( H is conjunctive implies ex G, H1 being LTL-formula st H1 '&' G = H )

proof

assume H is conjunctive ; :: thesis: ex G, H1 being LTL-formula st H1 '&' G = H
then consider G, F being LTL-formula such that
A7: G '&' F = H by Def13;
take F ; :: thesis: ex H1 being LTL-formula st H1 '&' F = H
thus ex H1 being LTL-formula st H1 '&' F = H by A7; :: thesis: verum

end;

( not H is conjunctive & not H is disjunctive & not H is Until implies ex G, H1 being LTL-formula st H1 'R' G = H )

proof

assume ( not H is conjunctive & not H is disjunctive & not H is Until ) ; :: thesis: ex G, H1 being LTL-formula st H1 'R' G = H
then consider G, F being LTL-formula such that
A8: G 'R' F = H by A1, Def17;
take F ; :: thesis: ex H1 being LTL-formula st H1 'R' F = H
thus ex H1 being LTL-formula st H1 'R' F = H by A8; :: thesis: verum

end;

hence ( ( H is conjunctive implies ex b₁, H1 being LTL-formula st H1 '&' b₁ = H ) & ( H is disjunctive implies ex b₁, H1 being LTL-formula st H1 'or' b₁ = H ) & ( H is Until implies ex b₁, H1 being LTL-formula st H1 'U' b₁ = H ) & ( not H is conjunctive & not H is disjunctive & not H is Until implies ex b₁, H1 being LTL-formula st H1 'R' b₁ = H ) ) by A6, A4, A2; :: thesis: verum