for a, b being Real holds Intersection (half_open_sets (a,b)) = [.a,b.]