theorem Th2: :: QC_LANG2:2

for A being QC-alphabet
for p, q, p1, q1 being Element of QC-WFF A st p '&' q = p1 '&' q1 holds
( p = p1 & q = q1 )