theorem Th37: :: SETWISEO:40

for A being set holds {}. A is_a_unity_wrt FinUnion A