theorem Th17: :: ALTCAT_1:23
( EnsCat {0} is pseudo-discrete & EnsCat {0} is 1 -element )