theorem Th40: :: SETWISEO:43

for A being set holds the_unity_wrt (FinUnion A) = {}