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

-infty is UpperBound of {} by Th37;

hence sup {} = -infty by A1, Def3; :: thesis: verum