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