:: deftheorem Def26 defines the_right_argument_of QC_LANG1:def 26 :
for A being QC-alphabet
for F being Element of QC-WFF A st F is conjunctive holds
for b₃ being QC-formula of A holds
( b₃ = the_right_argument_of F iff ex p being Element of QC-WFF A st F = p '&' b₃ );