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 19;
hence ( the_left_argument_of (p '&' q) = p & the_right_argument_of (p '&' q) = q ) by QC_LANG1:def 24, QC_LANG1:def 25; :: thesis: verum