thus ( H is conjunctive implies ex G, H1 being CTL-formula st H1 '&' G = H ) :: thesis: ( not H is conjunctive implies ex b₁, H1 being CTL-formula st H1 EU b₁ = H )

proof

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

end;

thus ( not H is conjunctive implies ex G, H1 being CTL-formula st H1 EU G = H ) :: thesis: verum

proof

assume not H is conjunctive ; :: thesis: ex G, H1 being CTL-formula st H1 EU G = H
then consider G, F being CTL-formula such that
A3: G EU F = H by A1, Def19;
take F ; :: thesis: ex H1 being CTL-formula st H1 EU F = H
thus ex H1 being CTL-formula st H1 EU F = H by A3; :: thesis: verum

end;