:: deftheorem defines FCEx GOEDCPUC:def 3 :
for Al being QC-alphabet holds FCEx Al = [:NAT,((QC-symbols Al) \/ { [ the free_symbol of Al,[x,p]] where p is Element of CQC-WFF Al, x is bound_QC-variable of Al : verum } ):];