A1:
for x being LowerBound of {} holds x <= +infty
by XXREAL_0:3;

+infty is LowerBound of {} by Th36;

hence inf {} = +infty by A1, Def4; :: thesis: verum

+infty is LowerBound of {} by Th36;

hence inf {} = +infty by A1, Def4; :: thesis: verum