:: deftheorem Def4 defines UNIVERSAL CQC_SIM1:def 4 :
for A being QC-alphabet
for f being Function of [:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)
for x being bound_QC-variable of A
for b₄ being Element of Funcs ([:(QC-symbols A),(Funcs ((bound_QC-variables A),(bound_QC-variables A))):],(CQC-WFF A)) holds
( b₄ = UNIVERSAL (x,f) iff for t being QC-symbol of A
for h being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))
for p being Element of CQC-WFF A st p = f . ((t ++),(h +* (x .--> (x. t)))) holds
b₄ . (t,h) = All ((x. t),p) );