theorem Th9: :: XXREAL_2:9

for A, B being ext-real-membered set holds inf (A \/ B) = min ((inf A),(inf B))