QC-WFF A is non empty A -closed set by Def11;
hence (<*[2,0]*> ^ (@ p)) ^ (@ q) is QC-formula of A by Def10; :: thesis: verum