theorem Th3: :: QC_LANG2:3

for A being QC-alphabet
for p being Element of QC-WFF A st p is conjunctive holds
p = (the_left_argument_of p) '&' (the_right_argument_of p)