:: deftheorem defines the_left_side_of QC_LANG2:def 17 :
for A being QC-alphabet
for H being Element of QC-WFF A holds the_left_side_of H = the_antecedent_of (the_left_argument_of H);