per cases ( A <> {} or A = {} ) ;

suppose A1: A <> {} ; :: thesis: r ** A is bounded_above

A c= REAL by MEMBERED:3;
hence r ** A is bounded_above by A1, INTEGRA2:9; :: thesis: verum

end;

suppose A = {} ; :: thesis: r ** A is bounded_above

hence r ** A is bounded_above ; :: thesis: verum

end;

end;