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