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

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

suppose X is trivial ; :: thesis: X is left_end

hence X is left_end by A2; :: thesis: verum

end;

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

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

proof

per cases ( N is Nat or N = +infty ) by Th3;

suppose N is Nat ; :: thesis: ex n being Nat st S₁[n]

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

end;

suppose A5: N = +infty ; :: thesis: ex n being Nat st S₁[n]

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: S₁[n]
thus S₁[n] by A6; :: thesis: verum

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: for x being ExtNat st x in X holds
n <= x

let x be ExtNat; :: thesis: ( x in X implies n <= b₁ )
assume A7a: x in X ; :: thesis: n <= b₁

per cases ( x is Nat or x = +infty ) by Th3;

suppose x is Nat ; :: thesis: n <= b₁

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

end;

suppose x = +infty ; :: thesis: n <= b₁

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

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: verum

end;

end;