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 consider n being Nat such that
A1: X,n are_equipotent by CARD_1:43;
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