theorem Th58: :: CQC_THE3:58

for A being QC-alphabet
for p, q being Element of CQC-WFF A
for x being bound_QC-variable of A st p <==> q holds
All (x,p) <==> All (x,q)