:: deftheorem defines Example_of GOEDCPUC:def 4 :
for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al holds Example_of (p,x) = [4,[ the free_symbol of Al,[x,p]]];