for b being Real holds Intersection (ext_half_open_sets b) = [.b,+infty.]