theorem Th72: :: XXREAL_2:72

for x, y being ExtReal
for A being ext-real-membered set st y <= x & x is LowerBound of A holds
y is LowerBound of A