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