for n being Nat holds Seg n,n are_equipotent by Lm1;