let H be LTL-formula; :: thesis: ( H is conjunctive implies H = (the_left_argument_of H) '&' (the_right_argument_of H) )
assume A1: H is conjunctive ; :: thesis: H = (the_left_argument_of H) '&' (the_right_argument_of H)
then ex H1 being LTL-formula st H = H1 '&' (the_right_argument_of H) by Def20;
hence H = (the_left_argument_of H) '&' (the_right_argument_of H) by A1, Def19; :: thesis: verum