consider x being bound_QC-variable, p being Element of CQC-WFF ;
set a = Ex x,p;
Ex x,p in ExCl by Def3;
hence not ExCl is empty ; :: thesis: ExCl is countable
thus ExCl is countable by Th19; :: thesis: verum