theorem Th13: :: CATALG_1:13

for a1, b1, a2, b2 being set st homsym (a1,a2) = homsym (b1,b2) holds
( a1 = b1 & a2 = b2 )