let Al be QC-alphabet ; :: thesis: ( Al is countable implies ( not ExCl Al is empty & ExCl Al is countable ) )
assume A1: Al is countable ; :: thesis: ( not ExCl Al is empty & ExCl Al is countable )
set x = the bound_QC-variable of Al;
set p = the Element of CQC-WFF Al;
set a = Ex ( the bound_QC-variable of Al, the Element of CQC-WFF Al);
Ex ( the bound_QC-variable of Al, the Element of CQC-WFF Al) in ExCl Al by Def3;
hence not ExCl Al is empty ; :: thesis: ExCl Al is countable
CQC-WFF Al is countable by Th19, A1;
hence ExCl Al is countable ; :: thesis: verum