A1: (left_open_halfline r) ` = right_closed_halfline r by XXREAL_1:224, XXREAL_1:290;
thus halfline r is open by A1, RCOMP_1:def 5; :: thesis: verum