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