theorem Th12: :: CATALG_1:12

for a, b being set st idsym a = idsym b holds
a = b