A1: for x being UpperBound of {} holds -infty <= x by XXREAL_0:5;
-infty is UpperBound of {} by Th37;
hence sup {} = -infty by A1, Def3; :: thesis: verum