let a be Real; :: thesis: ].-infty,a.] is closed
].-infty,a.] = left_closed_halfline a ;
hence ].-infty,a.] is closed ; :: thesis: verum