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