reconsider B = y=0-line as closed Subset of Niemytzki-plane by Th30;
let A be Subset of y=0-line ; :: thesis: A is closed Subset of Niemytzki-plane
A c= B ;
then reconsider A = A as Subset of Niemytzki-plane by XBOOLE_1:1;
Der A c= Der B by TOPGEN_1:32;
then Der A c= {} by Th45;
then Der A = {} ;
then Cl A = A \/ {} by TOPGEN_1:31;
hence A is closed Subset of Niemytzki-plane ; :: thesis: verum