theorem Th7: :: XXREAL_2:7

for A, B being ext-real-membered set
for x being LowerBound of A
for y being LowerBound of B holds min (x,y) is LowerBound of A \/ B