for A being QC-alphabet
for p, q being Element of QC-WFF A holds
( the_left_argument_of (p '&' q) = p & the_right_argument_of (p '&' q) = q )