[S,x] `1 = S by MCART_1:7;
hence [S,x] is CQC-WFF-like Element of [:QC-Sub-WFF ,bound_QC-variables :] by Def5; :: thesis: verum