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