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