let p, q be Element of QC-WFF ; :: thesis: ( the_left_argument_of (p '&' q) = p & the_right_argument_of (p '&' q) = q )
p '&' q is conjunctive by QC_LANG1:def 18;
hence ( the_left_argument_of (p '&' q) = p & the_right_argument_of (p '&' q) = q ) by QC_LANG1:def 23, QC_LANG1:def 24; :: thesis: verum