let X be natural-membered non empty set ; :: thesis: X is left_end
defpred S1[ set ] means c1 in X;
A1: ex k being Nat st S1[k] by MEMBERED:12;
consider k being Nat such that
A2: S1[k] and
A3: for n being Nat st S1[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