:: deftheorem Def3 defines . CQC_LANG:def 3 :
for A being QC-alphabet
for p being Element of QC-WFF A
for x being bound_QC-variable of A
for b₄ being Element of QC-WFF A holds
( b₄ = p . x iff ex F being Function of (QC-WFF A),(QC-WFF A) st
( b₄ = F . p & ( for q being Element of QC-WFF A holds
( F . (VERUM A) = VERUM A & ( q is atomic implies F . q = (the_pred_symbol_of q) ! (Subst ((the_arguments_of q),((A a. 0) .--> x))) ) & ( q is negative implies F . q = 'not' (F . (the_argument_of q)) ) & ( q is conjunctive implies F . q = (F . (the_left_argument_of q)) '&' (F . (the_right_argument_of q)) ) & ( q is universal implies F . q = IFEQ ((bound_in q),x,q,(All ((bound_in q),(F . (the_scope_of q))))) ) ) ) ) );