:: deftheorem Def23 defines the_right_argument_of MODELC_1:def 23 :
for H being CTL-formula st ( H is conjunctive or H is ExistUntill ) holds
for b₂ being CTL-formula holds
( ( H is conjunctive implies ( b₂ = the_right_argument_of H iff ex H1 being CTL-formula st H1 '&' b₂ = H ) ) & ( not H is conjunctive implies ( b₂ = the_right_argument_of H iff ex H1 being CTL-formula st H1 EU b₂ = H ) ) );