[S,x] in [:QC-Sub-WFF ,bound_QC-variables :] ;
hence [S,x] is Element of [:QC-Sub-WFF ,bound_QC-variables :] ; :: thesis: verum