let x be real number ; :: thesis: right_closed_halfline x is closed Subset of
set T = Sorgenfrey-line ;
reconsider A = left_open_halfline x as open Subset of by TOPGEN_3:13;
the carrier of Sorgenfrey-line = REAL by TOPGEN_3:def 2;
then ((right_closed_halfline x) ` ) ` = A ` by XXREAL_1:224, XXREAL_1:294;
hence right_closed_halfline x is closed Subset of ; :: thesis: verum