theorem Th18: :: NORMFORM:18

for A being set holds FinPairUnion A is having_a_unity