let Al be QC-alphabet ; :: thesis: for p being Element of CQC-WFF Al

for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st

( S `1 = p & S `2 = Sub )

defpred S_{1}[ Element of CQC-WFF Al] means for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st

( S `1 = $1 & S `2 = Sub );

A1: for p, q being Element of CQC-WFF Al

for x being bound_QC-variable of Al

for k being Nat

for ll being CQC-variable_list of k,Al

for P being QC-pred_symbol of k,Al holds

( S_{1}[ VERUM Al] & S_{1}[P ! ll] & ( S_{1}[p] implies S_{1}[ 'not' p] ) & ( S_{1}[p] & S_{1}[q] implies S_{1}[p '&' q] ) & ( S_{1}[p] implies S_{1}[ All (x,p)] ) )
by Th1, Th2, Th4, Th5, Th11;

thus for p being Element of CQC-WFF Al holds S_{1}[p]
from CQC_LANG:sch 1(A1); :: thesis: verum

for Sub being CQC_Substitution of Al ex S being Element of CQC-Sub-WFF Al st

( S `1 = p & S `2 = Sub )

defpred S

( S `1 = $1 & S `2 = Sub );

A1: for p, q being Element of CQC-WFF Al

for x being bound_QC-variable of Al

for k being Nat

for ll being CQC-variable_list of k,Al

for P being QC-pred_symbol of k,Al holds

( S

thus for p being Element of CQC-WFF Al holds S