theorem Th20: :: CQC_LANG:20

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