theorem :: CQC_THE2:57

for A being QC-alphabet
for p being Element of CQC-WFF A
for x, y being bound_QC-variable of A holds
( (Ex (x,(Ex (y,p)))) => (Ex (y,(Ex (x,p)))) is valid & (Ex (x,y,p)) => (Ex (y,x,p)) is valid )