:: deftheorem Def19 defines the_left_argument_of MODELC_2:def 19 :
for H being LTL-formula st ( H is conjunctive or H is disjunctive or H is Until or H is Release ) holds
for b₂ being LTL-formula holds
( ( H is conjunctive implies ( b₂ = the_left_argument_of H iff ex H1 being LTL-formula st b₂ '&' H1 = H ) ) & ( H is disjunctive implies ( b₂ = the_left_argument_of H iff ex H1 being LTL-formula st b₂ 'or' H1 = H ) ) & ( H is Until implies ( b₂ = the_left_argument_of H iff ex H1 being LTL-formula st b₂ 'U' H1 = H ) ) & ( not H is conjunctive & not H is disjunctive & not H is Until implies ( b₂ = the_left_argument_of H iff ex H1 being LTL-formula st b₂ 'R' H1 = H ) ) );