let A be Subset of Niemytzki-plane; :: thesis: ( A = y>=0-plane \ y=0-line implies for x being set holds Cl (A \ {x}) = [#] Niemytzki-plane )
assume A1: A = y>=0-plane \ y=0-line ; :: thesis: for x being set holds Cl (A \ {x}) = [#] Niemytzki-plane
let s be set ; :: thesis: Cl (A \ {s}) = [#] Niemytzki-plane
reconsider B = A /\ (product <*RAT,RAT*>) as Subset of Niemytzki-plane ;
thus Cl (A \ {s}) c= [#] Niemytzki-plane ; :: according to XBOOLE_0:def 10 :: thesis: [#] Niemytzki-plane c= Cl (A \ {s})
B \ {s} c= A \ {s} by XBOOLE_1:17, XBOOLE_1:33;
then Cl (B \ {s}) c= Cl (A \ {s}) by PRE_TOPC:19;
hence [#] Niemytzki-plane c= Cl (A \ {s}) by A1, Th32; :: thesis: verum