theorem Th3: :: TAXONOM2:4

for X being non empty set
for C, x being set st C is Classification of X & x in union C holds
x c= X