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