theorem Th38: :: SETWISEO:41

for A being set holds FinUnion A is having_a_unity