let a be Real; :: thesis: [.a,+infty.[ is closed
[.a,+infty.[ = right_closed_halfline a ;
hence [.a,+infty.[ is closed ; :: thesis: verum