theorem Th4: :: TREES_1:5

for x, y being set st <*x*>,<*y*> are_c=-comparable holds
x = y