let a be real number ; :: thesis: ].-infty ,a.[ is open
].-infty ,a.[ = left_open_halfline a ;
hence ].-infty ,a.[ is open ; :: thesis: verum