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