[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