X c= NAT by MEMBERED:6;
then consider d1, d2 being Element of NAT such that
A1: d1 in X and
A2: d2 in X and
A3: d1 <> d2 by SUBSET_1:45;

per cases ( d1 < d2 or d2 < d1 ) by A3, XXREAL_0:1;

suppose d1 < d2 ; :: thesis: ex b₁ being Subset of X st
( not b₁ is empty & b₁ is included_in_Seg )

then A4: 0 + 1 <= d2 by NAT_1:13;
reconsider A = {d2} as Subset of X by A2, ZFMISC_1:31;
take A ; :: thesis: ( not A is empty & A is included_in_Seg )
thus not A is empty ; :: thesis: A is included_in_Seg
take d2 ; :: according to FINSEQ_1:def 13 :: thesis: A c= Seg d2
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in Seg d2 )
assume x in A ; :: thesis: x in Seg d2
then x = d2 by TARSKI:def 1;
hence x in Seg d2 by A4; :: thesis: verum

end;

suppose d2 < d1 ; :: thesis: ex b₁ being Subset of X st
( not b₁ is empty & b₁ is included_in_Seg )

then A5: 0 + 1 <= d1 by NAT_1:13;
reconsider A = {d1} as Subset of X by A1, ZFMISC_1:31;
take A ; :: thesis: ( not A is empty & A is included_in_Seg )
thus not A is empty ; :: thesis: A is included_in_Seg
take d1 ; :: according to FINSEQ_1:def 13 :: thesis: A c= Seg d1
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in Seg d1 )
assume x in A ; :: thesis: x in Seg d1
then x = d1 by TARSKI:def 1;
hence x in Seg d1 by A5; :: thesis: verum

end;

end;