let X be finite natural-membered set ; :: thesis: ( X is with_non-empty_elements implies X is included_in_Seg )
assume A1: X is with_non-empty_elements ; :: thesis: X is included_in_Seg

per cases ( not X is empty or X is empty ) ;

suppose not X is empty ; :: thesis: X is included_in_Seg

then reconsider Y = X as non empty finite natural-membered set ;
reconsider k = max Y as Nat by TARSKI:1;
take k ; :: according to FINSEQ_1:def 13 :: thesis: X c= Seg k
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Seg k )
assume A2: x in X ; :: thesis: x in Seg k
then reconsider x = x as Nat ;
A3: 1 <= x by A1, A2, NAT_1:25;
x <= k by A2, XXREAL_2:def 8;
hence x in Seg k by A3; :: thesis: verum

end;

suppose X is empty ; :: thesis: X is included_in_Seg

hence X is included_in_Seg ; :: thesis: verum

end;

end;