let A be QC-alphabet ; :: thesis: for p being Element of QC-WFF A st p is conjunctive holds
p = (the_left_argument_of p) '&' (the_right_argument_of p)
let p be Element of QC-WFF A; :: thesis: ( p is conjunctive implies p = (the_left_argument_of p) '&' (the_right_argument_of p) )
given p1, q1 being Element of QC-WFF A such that A1: p = p1 '&' q1 ; :: according to QC_LANG1:def 20 :: thesis: p = (the_left_argument_of p) '&' (the_right_argument_of p)
A2: p is conjunctive by A1;
then p1 = the_left_argument_of p by A1, QC_LANG1:def 25;
hence p = (the_left_argument_of p) '&' (the_right_argument_of p) by A1, A2, QC_LANG1:def 26; :: thesis: verum