thus ( X is with_min implies ( X is bounded_below & lower_bound X in X ) ) :: thesis: ( X is bounded_below & lower_bound X in X implies X is with_min )

proof

assume A3: X is with_min ; :: thesis: ( X is bounded_below & lower_bound X in X )
hence X is bounded_below ; :: thesis: lower_bound X in X
reconsider X = X as non empty real-membered bounded_below set by A3;
lower_bound X in X by A3;
hence lower_bound X in X ; :: thesis: verum

end;

assume A4: ( X is bounded_below & lower_bound X in X ) ; :: thesis: X is with_min
then reconsider X = X as non empty real-membered bounded_below set ;
lower_bound X in X by A4;
hence X is with_min ; :: thesis: verum