theorem Th3: :: XXREAL_2:3

for x being ExtReal
for A being ext-real-membered set st x in A holds
inf A <= x