for r being Element of CQC-WFF F₁() holds P₁[r]

A1: P₁[ VERUM F₁()] and
A2: for k being Nat
for l being CQC-variable_list of k,F₁()
for P being QC-pred_symbol of k,F₁() holds P₁[P ! l] and
A3: for r being Element of CQC-WFF F₁() st P₁[r] holds
P₁[ 'not' r] and
A4: for r, s being Element of CQC-WFF F₁() st P₁[r] & P₁[s] holds
P₁[r '&' s] and
A5: for r being Element of CQC-WFF F₁()
for x being bound_QC-variable of F₁() st P₁[r] holds
P₁[ All (x,r)]