(y>=0-plane \ y=0-line) /\ (product <*RAT,RAT*>) c= y>=0-plane \ y=0-line by XBOOLE_1:17;
then reconsider A = (y>=0-plane \ y=0-line) /\ (product <*RAT,RAT*>) as Subset of Niemytzki-plane by Th25, XBOOLE_1:1;
A \ {A} = A
proof
thus A \ {A} c= A by XBOOLE_1:36; :: according to XBOOLE_0:def 10 :: thesis: A c= A \ {A}
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in A \ {A} )
not A in A ;
hence ( not x in A or x in A \ {A} ) by ZFMISC_1:56; :: thesis: verum
end;
then Cl A = [#] Niemytzki-plane by Th32;
hence (y>=0-plane \ y=0-line) /\ (product <*RAT,RAT*>) is dense Subset of Niemytzki-plane by TOPS_1:def 3; :: thesis: verum