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