the carrier of Niemytzki-plane = y>=0-plane by Def3;
then reconsider A = y>=0-plane \ y=0-line as Subset of Niemytzki-plane by XBOOLE_1:36;
A is dense-in-itself

proof

let a be object ; :: according to TARSKI:def 3,TOPGEN_1:def 7 :: thesis: ( not a in A or a in Der A )
assume a in A ; :: thesis: a in Der A
then reconsider x = a as Point of Niemytzki-plane ;
Cl (A \ {x}) = the carrier of Niemytzki-plane by Th33;
then x is_an_accumulation_point_of A ;
hence a in Der A by TOPGEN_1:def 3; :: thesis: verum

end;

hence y>=0-plane \ y=0-line is dense-in-itself Subset of Niemytzki-plane ; :: thesis: verum