(right_open_halfline r) ` = left_closed_halfline r by XXREAL_1:224, XXREAL_1:296;
hence right_open_halfline r is open ; :: thesis: verum