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