for m, n being Nat st Seg n, Seg m are_equipotent holds
n = m