reconsider B = real-anti-diagonal as closed Subset of Sorgenfrey-plane by Th4;

let A be Subset of real-anti-diagonal; :: thesis: A is closed Subset of Sorgenfrey-plane

A c= B ;

then reconsider A = A as Subset of Sorgenfrey-plane by XBOOLE_1:1;

Der A c= Der B by TOPGEN_1:30;

then Der A c= {} by Th5;

then Der A = {} ;

then Cl A = A \/ {} by TOPGEN_1:29;

hence A is closed Subset of Sorgenfrey-plane ; :: thesis: verum

let A be Subset of real-anti-diagonal; :: thesis: A is closed Subset of Sorgenfrey-plane

A c= B ;

then reconsider A = A as Subset of Sorgenfrey-plane by XBOOLE_1:1;

Der A c= Der B by TOPGEN_1:30;

then Der A c= {} by Th5;

then Der A = {} ;

then Cl A = A \/ {} by TOPGEN_1:29;

hence A is closed Subset of Sorgenfrey-plane ; :: thesis: verum