let A be QC-alphabet ; :: thesis: QC-WFF A is Subset of ([:NAT,(QC-symbols A):] *)
A1: QC-WFF A is non empty A -closed set by Def11;
thus QC-WFF A is Subset of ([:NAT,(QC-symbols A):] *) by A1, Def10; :: thesis: verum