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