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