let x, y be Real; :: thesis: [.x,y.[ is closed Subset of Sorgenfrey-line
set T = Sorgenfrey-line ;
reconsider A = right_closed_halfline x, B = left_open_halfline y as closed Subset of Sorgenfrey-line by Th54, Th56;
A1: the carrier of Sorgenfrey-line = REAL by TOPGEN_3:def 2;
[.x,y.[ = ([.x,y.[ `) `
.= ((left_open_halfline x) \/ (right_closed_halfline y)) ` by XXREAL_1:382
.= ((left_open_halfline x) `) /\ ((right_closed_halfline y) `) by XBOOLE_1:53
.= ((A `) `) /\ ((right_closed_halfline y) `) by A1, XXREAL_1:224, XXREAL_1:294
.= A /\ B by XXREAL_1:224, XXREAL_1:294 ;
hence [.x,y.[ is closed Subset of Sorgenfrey-line ; :: thesis: verum