[S,x] `1 = S ;
hence [S,x] is CQC-WFF-like Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):] by Def4; :: thesis: verum