theorem Th4: :: XXREAL_2:4

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