let X be ext-natural-membered set ; :: thesis:
assume not X is empty ; :: thesis:
then consider N being ExtNat such that
A2: N in X by ThEx;

per cases ;

suppose X is trivial ; :: thesis:

hence X is left_end by A2; :: thesis:

end;

suppose A3: not X is trivial ; :: thesis:

defpred S₁[ Nat] means c₁ in X;
A4: ex n being Nat st S₁[n]

proof

per cases by Th3;

suppose N is Nat ; :: thesis:

then reconsider n = N as Nat ;
take n ; :: thesis:
thus S₁[n] by A2; :: thesis:

end;

suppose A5: N = +infty ; :: thesis:

set n = the Element of X \ {N};
not X \ {N} is empty by A3, ZFMISC_1:139;
then A6: ( the Element of X \ {N} in X & the Element of X \ {N} <> +infty ) by A5, ZFMISC_1:56;
then reconsider n = the Element of X \ {N} as Nat by Th3;
take n ; :: thesis:
thus S₁[n] by A6; :: thesis:

end;

end;

end;

consider n being Nat such that
A7: ( S₁[n] & ( for m being Nat st S₁[m] holds
n <= m ) ) from NAT_1:sch 5(A4);

now :: thesis:

let x be ExtNat; :: thesis:
assume A7a: x in X ; :: thesis:

per cases by Th3;

suppose x is Nat ; :: thesis:

hence n <= x by A7, A7a; :: thesis:

end;

suppose x = +infty ; :: thesis:

hence n <= x by XXREAL_0:3; :: thesis:

end;

end;

end;

then A8: n is LowerBound of X by DefL;
for x being LowerBound of X holds x <= n by A7, XXREAL_2:def 2;
then inf X = n by A8, XXREAL_2:def 4;
hence X is left_end by A7, XXREAL_2:def 5; :: thesis:

end;

end;