theorem Th3: :: TREES_1:4

for p, q being finite set st p,q are_c=-comparable & card p = card q holds
p = q by CARD_2:102;