let p be Element of QC-WFF ; :: thesis: ( p is conjunctive implies p = (the_left_argument_of p) '&' (the_right_argument_of p) )
given p1, q1 being Element of QC-WFF such that A1: p = p1 '&' q1 ; :: according to QC_LANG1:def 19 :: thesis: p = (the_left_argument_of p) '&' (the_right_argument_of p)
( p is conjunctive & ex q being Element of QC-WFF st p = p1 '&' q & ex q being Element of QC-WFF st p = q '&' q1 ) by A1, QC_LANG1:def 19;
then ( p1 = the_left_argument_of p & q1 = the_right_argument_of p ) by QC_LANG1:def 24, QC_LANG1:def 25;
hence p = (the_left_argument_of p) '&' (the_right_argument_of p) by A1; :: thesis: verum