theorem Th16: :: UNIFORM3:32

for X being set
for D being a_partition of X st D = {} holds
( X is empty & UniCl D = {{}} ) by ZFMISC_1:2, EQREL_1:def 4, YELLOW_9:16;