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