A: +infty is LowerBound of {} by TW1;
for x being LowerBound of {} holds x <= +infty by XXREAL_0:3;
hence inf {} = +infty by A, Def4; :: thesis: verum