scheme :: CQC_LANG:sch 6
CQCDefatomic{ F₁() -> QC-alphabet , F₂() -> non empty set , F₃() -> Element of F₂(), F₄( set ) -> Element of F₂(), F₅( set , set , set ) -> Element of F₂(), F₆() -> Nat, F₇() -> QC-pred_symbol of F₆(),F₁(), F₈() -> CQC-variable_list of F₆(),F₁(), F₉( set ) -> Element of F₂(), F₁₀( set , set ) -> Element of F₂(), F₁₁( set , set ) -> Element of F₂() } :

F₄((F₇() ! F₈())) = F₅(F₆(),F₇(),F₈())

provided

A1: for p being Element of CQC-WFF F₁()
for d being Element of F₂() holds
( d = F₄(p) iff ex F being Function of (CQC-WFF F₁()),F₂() st
( d = F . p & F . (VERUM F₁()) = F₃() & ( for r, s being Element of CQC-WFF F₁()
for x being bound_QC-variable of F₁()
for k being Nat
for l being CQC-variable_list of k,F₁()
for P being QC-pred_symbol of k,F₁() holds
( F . (P ! l) = F₅(k,P,l) & F . ('not' r) = F₉((F . r)) & F . (r '&' s) = F₁₀((F . r),(F . s)) & F . (All (x,r)) = F₁₁(x,(F . r)) ) ) ) )