thus ( X is with_max implies ( X is bounded_above & upper_bound X in X ) ) :: thesis: ( X is bounded_above & upper_bound X in X implies X is with_max )

proof

assume A1: X is with_max ; :: thesis: ( X is bounded_above & upper_bound X in X )
hence X is bounded_above ; :: thesis: upper_bound X in X
reconsider X = X as non empty real-membered bounded_above set by A1;
upper_bound X in X by A1;
hence upper_bound X in X ; :: thesis: verum

end;

assume A2: ( X is bounded_above & upper_bound X in X ) ; :: thesis: X is with_max
then reconsider X = X as non empty real-membered bounded_above set ;
upper_bound X in X by A2;
hence X is with_max ; :: thesis: verum