set M = the non limit_cardinal Aleph;
take the non limit_cardinal Aleph ; :: thesis: ( the non limit_cardinal Aleph is regular & not the non limit_cardinal Aleph is countable )
thus ( the non limit_cardinal Aleph is regular & not the non limit_cardinal Aleph is countable ) ; :: thesis: verum