theorem Th60: :: FINANCE5:12

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