let A be QC-alphabet ; :: thesis: for p, q being Element of QC-WFF A holds
( the_left_argument_of (p '&' q) = p & the_right_argument_of (p '&' q) = q )
let p, q be Element of QC-WFF A; :: thesis: ( the_left_argument_of (p '&' q) = p & the_right_argument_of (p '&' q) = q )
p '&' q is conjunctive ;
hence ( the_left_argument_of (p '&' q) = p & the_right_argument_of (p '&' q) = q ) by QC_LANG1:def 25, QC_LANG1:def 26; :: thesis: verum