let X be natural-membered non empty set ; :: thesis: X is left_end
defpred S₁[ set ] means c₁ in X;
A1: ex k being Nat st S₁[k] by MEMBERED:12;
consider k being Nat such that
A2: S₁[k] and
A3: for n being Nat st S₁[n] holds
k <= n from NAT_1:sch 5(A1);
A4: k is LowerBound of X

proof

let y be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( y in X implies k <= y )
assume y in X ; :: thesis: k <= y
hence k <= y by A3; :: thesis: verum

end;

for x being LowerBound of X holds x <= k by A2, Def2;
hence inf X in X by A2, A4, Def4; :: according to XXREAL_2:def 5 :: thesis: verum