for A being QC-alphabet
for x, y, z being bound_QC-variable of A
for p, q being Element of QC-WFF A
for s, t being bound_QC-variable of A st Ex (x,y,z,p) = Ex (t,s,q) holds
( x = t & y = s & Ex (z,p) = q )