let X be set ; :: thesis: ( X is finite implies ex n being Nat st X, Seg n are_equipotent )
assume X is finite ; :: thesis: ex n being Nat st X, Seg n are_equipotent
then reconsider n = card X as Nat ;
A1: X,n are_equipotent by CARD_1:def 2;
take n ; :: thesis: X, Seg n are_equipotent
n, Seg n are_equipotent by Lm1;
hence X, Seg n are_equipotent by A1, WELLORD2:15; :: thesis: verum