theorem :: CQC_THE2:13

for A being QC-alphabet
for s, h being QC-formula of A
for x being bound_QC-variable of A holds (s 'or' h) . x = (s . x) 'or' (h . x)