:: deftheorem defines Example_Formulae_of GOEDCPUC:def 6 :
for Al being QC-alphabet holds Example_Formulae_of Al = { (Example_Formula_of (p,x)) where p is Element of CQC-WFF Al, x is bound_QC-variable of Al : verum } ;