:: deftheorem Def25 defines the_left_argument_of QC_LANG1:def 25 :
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_left_argument_of F iff ex q being Element of QC-WFF A st F = b₃ '&' q );