set T = Sorgenfrey-line ;
A1: the carrier of Sorgenfrey-line = REAL by TOPGEN_3:def 2;
let x be real number ; :: thesis: left_closed_halfline x is closed Subset of Sorgenfrey-line
reconsider A = right_open_halfline x as open Subset of Sorgenfrey-line by TOPGEN_3:14;
((left_closed_halfline x) ` ) ` = A ` by A1, XXREAL_1:224, XXREAL_1:288;
hence left_closed_halfline x is closed Subset of Sorgenfrey-line ; :: thesis: verum