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