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