theorem :: QC_LANG2:24

for A being QC-alphabet
for p1, p2 being Element of QC-WFF A
for x1, x2, y1, y2, z1, z2 being bound_QC-variable of A st Ex (x1,y1,z1,p1) = Ex (x2,y2,z2,p2) holds
( x1 = x2 & y1 = y2 & z1 = z2 & p1 = p2 )