let X be natural-membered non empty set ; :: thesis: X is left_end

defpred S_{1}[ set ] means c_{1} in X;

A1: ex k being Nat st S_{1}[k]
by MEMBERED:12;

consider k being Nat such that

A2: S_{1}[k]
and

A3: for n being Nat st S_{1}[n] holds

k <= n from NAT_1:sch 5(A1);

A4: k is LowerBound of X

hence inf X in X by A2, A4, Def4; :: according to XXREAL_2:def 5 :: thesis: verum

defpred S

A1: ex k being Nat st S

consider k being Nat such that

A2: S

A3: for n being Nat st S

k <= n from NAT_1:sch 5(A1);

A4: k is LowerBound of X

proof

for x being LowerBound of X holds x <= k
by A2, Def2;
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;assume y in X ; :: thesis: k <= y

hence k <= y by A3; :: thesis: verum

hence inf X in X by A2, A4, Def4; :: according to XXREAL_2:def 5 :: thesis: verum