theorem Th17: :: ALTCAT_1:23

( EnsCat {0} is pseudo-discrete & EnsCat {0} is 1 -element )