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